diff --git a/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst b/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst
new file mode 100644
index 0000000000000..8a3ec953076cd
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+ Ltac2 are typechecked at declaration time by default.
+ This should produce better errors when a notation argument does not have the expected type
+ (e.g. wrong branch type in `match! goal`).
+ The previous behaviour of typechecking only the expansion result can be
+ recovered using :flag:`Ltac2 Typed Notations`. We believe there are no real
+ use cases for this, please report if you have any
+ (`#18432 `_,
+ fixes `#17477 `_,
+ by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index ddff80741688c..aa4e5effe2176 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1220,11 +1220,22 @@ Notations
side (before the `:=`) defines the syntax to recognize and gives formal parameter
names for the syntactic values. :n:`@integer` is the level of the notation.
When the notation is used, the values are substituted
- into the right-hand side. The right-hand side is typechecked when the notation is used,
- not when it is defined. In the following example, `x` is the formal parameter name and
+ into the right-hand side. In the following example, `x` is the formal parameter name and
`constr` is its :ref:`syntactic class`. `print` and `of_constr` are
functions provided by Coq through `Message.v`.
+ .. flag:: Ltac2 Typed Notations
+
+ By default Ltac2 notations are typechecked at declaration time.
+ This assigns an expected type to notation arguments.
+
+ When a notation is declared with this flag unset, it is not
+ typechecked at declaration time and its expansion is typechecked
+ when it is used. This may allow slightly more flexible use of
+ the notation arguments at the cost of worse error messages when
+ incorrectly using the notation. It is not believed to be useful
+ in practice, please report any real use cases you find.
+
.. todo "print" doesn't seem to pay attention to "Set Printing All"
.. example:: Printing a :n:`@term`
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 5eb225bee3920..8759df94bde38 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -717,6 +717,7 @@ through the Require Import command.
theories/Compat/Coq818.v
theories/Compat/Coq819.v
user-contrib/Ltac2/Compat/Coq818.v
+ user-contrib/Ltac2/Compat/Coq819.v
Array:
diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml
index 079061b7b2c87..029a11f4eecab 100644
--- a/plugins/ltac2/tac2entries.ml
+++ b/plugins/ltac2/tac2entries.ml
@@ -674,7 +674,7 @@ let perform_notation syn st =
| Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
in
let map (na, e) =
- ((CAst.make ?loc:e.loc @@ CPatVar na), e)
+ ((CAst.make ?loc:e.loc na), e)
in
let bnd = List.map map args in
CAst.make ~loc @@ CTacSyn (bnd, syn.synext_kn)
@@ -721,8 +721,19 @@ let cache_synext_interp (local,kn,tac) =
let open_synext_interp i o =
if Int.equal i 1 then cache_synext_interp o
+let subst_notation_data subst = function
+ | Tac2env.UntypedNota body as n ->
+ let body' = Tac2intern.subst_rawexpr subst body in
+ if body' == body then n else UntypedNota body'
+ | TypedNota { nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body } as n ->
+ let body' = Tac2intern.subst_expr subst body in
+ let argtys' = Id.Map.Smart.map (subst_type subst) argtys in
+ let ty' = subst_type subst ty in
+ if body' == body && argtys' == argtys && ty' == ty then n
+ else TypedNota {nota_body=body'; nota_argtys=argtys'; nota_ty=ty'; nota_prms=prms}
+
let subst_synext_interp (subst, (local,kn,tac as o)) =
- let tac' = Tac2intern.subst_rawexpr subst tac in
+ let tac' = subst_notation_data subst tac in
let kn' = Mod_subst.subst_kn subst kn in
if kn' == kn && tac' == tac then o else
(local, kn', tac')
@@ -730,7 +741,7 @@ let subst_synext_interp (subst, (local,kn,tac as o)) =
let classify_synext_interp (local,_,_) =
if local then Dispose else Substitute
-let inTac2NotationInterp : (bool*KerName.t*raw_tacexpr) -> obj =
+let inTac2NotationInterp : (bool*KerName.t*Tac2env.notation_data) -> obj =
declare_object {(default_object "TAC2-NOTATION-INTERP") with
cache_function = cache_synext_interp;
open_function = simple_open ~cat:ltac2_notation_cat open_synext_interp;
@@ -837,8 +848,8 @@ let register_notation_interpretation = function
let abbr = { abbr_body = body; abbr_depr = deprecation } in
Lib.add_leaf (inTac2Abbreviation id abbr)
| Synext (local,kn,ids,body) ->
- let body = Tac2intern.globalize ids body in
- Lib.add_leaf (inTac2NotationInterp (local,kn,body))
+ let data = intern_notation_data ids body in
+ Lib.add_leaf (inTac2NotationInterp (local,kn,data))
type redefinition = {
redef_kn : ltac_constant;
diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml
index 775725ffb1bdc..b9965b2ecdd5a 100644
--- a/plugins/ltac2/tac2env.ml
+++ b/plugins/ltac2/tac2env.ml
@@ -65,6 +65,15 @@ let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
let compiled_tacs = Summary.ref ~local:true ~name:"ltac2-compiled-state" KNmap.empty
+type notation_data =
+ | UntypedNota of raw_tacexpr
+ | TypedNota of {
+ nota_prms : int;
+ nota_argtys : int glb_typexpr Id.Map.t;
+ nota_ty : int glb_typexpr;
+ nota_body : glb_tacexpr;
+ }
+
let ltac_notations = Summary.ref KNmap.empty ~stage:Summary.Stage.Synterp ~name:"ltac2-notations"
let define_global kn e =
diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli
index 555a014e12d64..7356208ba3ad6 100644
--- a/plugins/ltac2/tac2env.mli
+++ b/plugins/ltac2/tac2env.mli
@@ -95,8 +95,18 @@ val interp_alias : ltac_constant -> alias_data
(** {5 Toplevel definition of notations} *)
-val define_notation : ltac_notation -> raw_tacexpr -> unit
-val interp_notation : ltac_notation -> raw_tacexpr
+(* no deprecation info: deprecation warning is emitted by the parser *)
+type notation_data =
+ | UntypedNota of raw_tacexpr
+ | TypedNota of {
+ nota_prms : int;
+ nota_argtys : int glb_typexpr Id.Map.t;
+ nota_ty : int glb_typexpr;
+ nota_body : glb_tacexpr;
+ }
+
+val define_notation : ltac_notation -> notation_data -> unit
+val interp_notation : ltac_notation -> notation_data
(** {5 Name management} *)
diff --git a/plugins/ltac2/tac2expr.mli b/plugins/ltac2/tac2expr.mli
index 6a439adf51836..bc2df44b2ec3e 100644
--- a/plugins/ltac2/tac2expr.mli
+++ b/plugins/ltac2/tac2expr.mli
@@ -89,41 +89,6 @@ type atom =
| AtmInt of int
| AtmStr of string
-(** Tactic expressions *)
-type raw_patexpr_r =
-| CPatVar of Name.t
-| CPatAtm of atom
-| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
-| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
-| CPatCnv of raw_patexpr * raw_typexpr
-| CPatOr of raw_patexpr list
-| CPatAs of raw_patexpr * lident
-
-and raw_patexpr = raw_patexpr_r CAst.t
-
-type raw_tacexpr_r =
-| CTacAtm of atom
-| CTacRef of tacref or_relid
-| CTacCst of ltac_constructor or_tuple or_relid
-| CTacFun of raw_patexpr list * raw_tacexpr
-| CTacApp of raw_tacexpr * raw_tacexpr list
-| CTacSyn of (raw_patexpr * raw_tacexpr) list * KerName.t
-| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
-| CTacCnv of raw_tacexpr * raw_typexpr
-| CTacSeq of raw_tacexpr * raw_tacexpr
-| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
-| CTacCse of raw_tacexpr * raw_taccase list
-| CTacRec of raw_tacexpr option * raw_recexpr
-| CTacPrj of raw_tacexpr * ltac_projection or_relid
-| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
-
-and raw_tacexpr = raw_tacexpr_r CAst.t
-
-and raw_taccase = raw_patexpr * raw_tacexpr
-
-and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
-
(* We want to generate these easily in the Closed case, otherwise we
could have the kn in the ctor_data_for_patterns type. Maybe still worth doing?? *)
type ctor_indx =
@@ -180,6 +145,44 @@ type glb_tacexpr =
| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
| GTacPrm of ml_tactic_name
+(** Tactic expressions *)
+type raw_patexpr_r =
+| CPatVar of Name.t
+| CPatAtm of atom
+| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
+| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
+| CPatCnv of raw_patexpr * raw_typexpr
+| CPatOr of raw_patexpr list
+| CPatAs of raw_patexpr * lident
+
+and raw_patexpr = raw_patexpr_r CAst.t
+
+type raw_tacexpr_r =
+| CTacAtm of atom
+| CTacRef of tacref or_relid
+| CTacCst of ltac_constructor or_tuple or_relid
+| CTacFun of raw_patexpr list * raw_tacexpr
+| CTacApp of raw_tacexpr * raw_tacexpr list
+| CTacSyn of (lname * raw_tacexpr) list * KerName.t
+| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
+| CTacCnv of raw_tacexpr * raw_typexpr
+| CTacSeq of raw_tacexpr * raw_tacexpr
+| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
+| CTacCse of raw_tacexpr * raw_taccase list
+| CTacRec of raw_tacexpr option * raw_recexpr
+| CTacPrj of raw_tacexpr * ltac_projection or_relid
+| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
+| CTacGlb of int * (lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
+(** CTacGlb is essentially an expanded typed notation.
+ Arguments bound with Anonymous have no type constraint. *)
+
+and raw_tacexpr = raw_tacexpr_r CAst.t
+
+and raw_taccase = raw_patexpr * raw_tacexpr
+
+and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
+
(** {5 Parsing & Printing} *)
type exp_level =
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index a20129a9082d7..e214e72b56fc8 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1079,6 +1079,25 @@ let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with
str "All the fields are explicitly listed in this record:" ++
spc() ++ str "the 'with' clause is useless.")
+let expand_notation ?loc el kn =
+ match Tac2env.interp_notation kn with
+ | UntypedNota body ->
+ let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
+ let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ v
+ | TypedNota {nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body} ->
+ let argtys, el = List.fold_left_map (fun argtys (na,arg) ->
+ let argty, argtys = match na.CAst.v with
+ | Anonymous -> None, argtys
+ | Name id -> Some (Id.Map.get id argtys), Id.Map.remove id argtys
+ in
+ argtys ,(na, arg, argty))
+ argtys
+ el
+ in
+ assert (Id.Map.is_empty argtys);
+ CAst.make ?loc @@ CTacGlb (prms, el, body, ty)
+
let rec intern_rec env tycon {loc;v=e} =
let check et = check ?loc env tycon et in
match e with
@@ -1175,8 +1194,7 @@ let rec intern_rec env tycon {loc;v=e} =
if is_rec then intern_let_rec env el tycon e
else intern_let env loc ids el tycon e
| CTacSyn (el, kn) ->
- let body = Tac2env.interp_notation kn in
- let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ let v = expand_notation ?loc el kn in
intern_rec env tycon v
| CTacCnv (e, tc) ->
let tc = intern_type env tc in
@@ -1306,6 +1324,28 @@ let rec intern_rec env tycon {loc;v=e} =
| GlbTacexpr e -> e
in
check (e, tpe)
+| CTacGlb (prms, args, body, ty) ->
+ let tysubst = Array.init prms (fun _ -> fresh_id env) in
+ let tysubst i = GTypVar tysubst.(i) in
+ let ty = subst_type tysubst ty in
+ let ty = match tycon with
+ | None -> ty
+ | Some tycon ->
+ let () = unify ?loc env ty tycon in
+ tycon
+ in
+ let args = List.map (fun (na, arg, ty) ->
+ let ty = Option.map (subst_type tysubst) ty in
+ let () = match na.CAst.v, ty with
+ | Anonymous, None | Name _, Some _ -> ()
+ | Anonymous, Some _ | Name _, None -> assert false
+ in
+ let e, _ = intern_rec env ty arg in
+ na.CAst.v, e)
+ args
+ in
+ if CList.is_empty args then body, ty
+ else GTacLet (false, args, body), ty
and intern_rec_with_constraint env e exp =
let (er, t) = intern_rec env (Some exp) e in
@@ -1592,8 +1632,7 @@ let globalize_gen ~tacext ids tac =
let bnd = List.map map bnd in
CAst.make ?loc @@ CTacLet (isrec, bnd, e)
| CTacSyn (el, kn) ->
- let body = Tac2env.interp_notation kn in
- let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ let v = expand_notation ?loc el kn in
globalize ids v
| CTacCnv (e, t) ->
let e = globalize ids e in
@@ -1629,6 +1668,9 @@ let globalize_gen ~tacext ids tac =
let e' = globalize ids e' in
CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
| CTacExt (tag, arg) -> tacext ?loc (RawExt (tag, arg))
+ | CTacGlb (prms, args, body, ty) ->
+ let args = List.map (fun (na, arg, ty) -> na, globalize ids arg, ty) args in
+ CAst.make ?loc @@ CTacGlb (prms, args, body, ty)
and globalize_case ids (p, e) =
(globalize_pattern ids p, globalize ids e)
@@ -1670,6 +1712,35 @@ let debug_globalize_allow_ext ids tac =
let tacext ?loc (RawExt (tag,arg)) = CAst.make ?loc @@ CTacExt (tag,arg) in
globalize_gen ~tacext ids tac
+let { Goptions.get = typed_notations } =
+ Goptions.declare_bool_option_and_ref
+ ~key:["Ltac2";"Typed";"Notations"] ~value:true ()
+
+let intern_notation_data ids body =
+ if typed_notations () then
+ let env = empty_env ~strict:true () in
+ let fold id (env,argtys) =
+ let ty = GTypVar (fresh_id env) in
+ let env = push_name (Name id) (monomorphic ty) env in
+ env, Id.Map.add id ty argtys
+ in
+ let env, argtys = Id.Set.fold fold ids (env,Id.Map.empty) in
+ let body, ty = intern_rec env None body in
+ let count = ref 0 in
+ let vars = ref TVar.Map.empty in
+ let argtys = Id.Map.map (fun ty -> normalize env (count, vars) ty) argtys in
+ let ty = normalize env (count, vars) ty in
+ let prms = !count in
+ Tac2env.TypedNota {
+ nota_prms = prms;
+ nota_argtys = argtys;
+ nota_ty = ty;
+ nota_body = body;
+ }
+ else
+ let body = globalize ids body in
+ Tac2env.UntypedNota body
+
(** Kernel substitution *)
open Mod_subst
@@ -1924,6 +1995,18 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
let e' = subst_rawexpr subst e in
let r' = subst_rawexpr subst r in
if prj' == prj && e' == e && r' == r then t else CAst.make ?loc @@ CTacSet (e', prj', r')
+| CTacGlb (prms, args, body, ty) ->
+ let args' = List.Smart.map (fun (na, arg, ty as o) ->
+ let arg' = subst_rawexpr subst arg in
+ let ty' = Option.Smart.map (subst_type subst) ty in
+ if arg' == arg && ty' == ty then o
+ else (na, arg', ty'))
+ args
+ in
+ let body' = subst_expr subst body in
+ let ty' = subst_type subst ty in
+ if args' == args && body' == body && ty' == ty then t
+ else CAst.make ?loc @@ CTacGlb (prms, args', body', ty')
| CTacSyn _ | CTacExt _ -> assert false (** Should not be generated by globalization *)
(** Registering *)
diff --git a/plugins/ltac2/tac2intern.mli b/plugins/ltac2/tac2intern.mli
index 22a082f2bafbb..58a2ff58949da 100644
--- a/plugins/ltac2/tac2intern.mli
+++ b/plugins/ltac2/tac2intern.mli
@@ -17,6 +17,7 @@ type context = (Id.t * type_scheme) list
val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme
val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
val intern_open_type : raw_typexpr -> type_scheme
+val intern_notation_data : Id.Set.t -> raw_tacexpr -> Tac2env.notation_data
(** Check that a term is a value. Only values are safe to marshall between
processes. *)
diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml
index 540507a99f2b3..54d6743d9fc5f 100644
--- a/plugins/ltac2/tac2print.ml
+++ b/plugins/ltac2/tac2print.ml
@@ -575,6 +575,8 @@ let rec pr_rawpat_gen lvl p = match p.CAst.v with
in
paren (hv 0 (pr_rawpat_gen E1 p ++ spc() ++ str "as" ++ spc () ++ Id.print x.v))
+(* XXX in principle we could have collisions with user names *)
+let base_internal_ty_ident = Id.of_string "__α"
let pr_rawexpr_gen lvl ~avoid c =
let rec pr_rawexpr lvl avoid c =
@@ -699,6 +701,32 @@ let pr_rawexpr_gen lvl ~avoid c =
let env = Global.env() in
let sigma = Evd.from_env env in
obj.ml_raw_print env sigma arg
+ | CTacGlb (prms, args, body, ty) ->
+ let avoid, tynames =
+ Array.fold_left_map (fun avoid () ->
+ let na = Namegen.next_ident_away base_internal_ty_ident avoid in
+ let avoid = Id.Set.add na avoid in
+ avoid, Id.to_string na)
+ avoid
+ (Array.make prms ())
+ in
+ let tynames i = tynames.(i) in
+ let pr_arg (pat, arg, ty) =
+ let bnd = match ty with
+ | Some ty ->
+ paren (pr_name pat.CAst.v ++ spc() ++ str ":" ++ spc() ++ pr_glbtype_gen tynames T5_l ty)
+ | None -> pr_name pat.CAst.v
+ in
+ bnd ++ spc() ++ str ":=" ++ spc() ++ hov 2 (pr_rawexpr E5 avoid arg) ++ spc()
+ in
+ let paren = match lvl with
+ | E0 | E1 | E2 | E3 | E4 -> paren
+ | E5 -> fun x -> x
+ in
+ let bnd = prlist_with_sep (fun () -> str "with" ++ spc ()) pr_arg args in
+ paren (hv 0 (hov 2 (str "let" ++ spc() ++ bnd ++ str "in") ++ spc()
+ ++ pr_glbexpr_gen ~avoid E5 body ++ spc()
+ ++ str ":" ++ pr_glbtype_gen tynames T5_l ty))
in
hov 0 (pr_rawexpr lvl avoid c)
diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml
index cd6e6e4925252..0fab69cfc8fac 100644
--- a/plugins/ltac2/tac2quote.ml
+++ b/plugins/ltac2/tac2quote.ml
@@ -450,10 +450,7 @@ let of_constr_matching {loc;v=m} =
of_tuple [knd; pat; e]
in
let e = of_list ?loc map m in
- let tykn = pattern_core "constr_matching" in
- let ty = CAst.make ?loc (CTypRef (AbsKn (Other tykn),[CAst.make ?loc (CTypVar Anonymous)])) in
- CAst.make ?loc (CTacCnv (e, ty))
-
+ e
(** From the patterns and the body of the branch, generate:
- a goal pattern: (constr_match list * constr_match)
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index 6e5e796d82b8d..326c423d43ed5 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -241,6 +241,7 @@ let get_compat_file = function
let get_compat_files v =
let coq_compat = get_compat_file v in
match v with
+ | "8.19" -> coq_compat :: ["Ltac2.Compat.Coq819"]
| "8.18" | "8.17" -> coq_compat :: ["Ltac2.Compat.Coq818"]
| _ -> [coq_compat]
diff --git a/test-suite/output/ltac2_check_globalize.out b/test-suite/output/ltac2_check_globalize.out
index cf70cba87c4f8..b5a8f75bbb237 100644
--- a/test-suite/output/ltac2_check_globalize.out
+++ b/test-suite/output/ltac2_check_globalize.out
@@ -4,7 +4,7 @@ fun x => x : 'a -> 'a
() ()
(1, 2) 3
let x := () in x ()
-File "./output/ltac2_check_globalize.v", line 20, characters 32-33:
+File "./output/ltac2_check_globalize.v", line 22, characters 32-33:
The command has indeed failed with message:
This expression has type unit. It is not a function and cannot be applied.
let x := fun x => x in let _ := x 1 in let _ := x "" in ()
@@ -13,11 +13,11 @@ let accu := { contents := []} in
(let x := fun x => accu.(contents) := (x :: accu.(contents)) in
let _ := x 1 in let _ := x "" in ());
accu.(contents)
-File "./output/ltac2_check_globalize.v", line 36, characters 0-144:
+File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
The command has indeed failed with message:
This expression has type string but an expression was expected of type
int
-let m :=
+let (m : '__α Pattern.goal_matching) :=
[(([(None, (Pattern.MatchPattern, pat:(_)))],
(Pattern.MatchPattern, pat:(_))),
(fun h =>
@@ -27,4 +27,5 @@ let m :=
(fun _ => fun _ => fun _ => fun _ => fun _ => ()))] : _
Pattern.goal_matching in
Pattern.lazy_goal_match0 false m
+:'__α
constr:(ltac2:(()))
diff --git a/test-suite/output/ltac2_check_globalize.v b/test-suite/output/ltac2_check_globalize.v
index 72ffc0d62f836..cbeea4f065812 100644
--- a/test-suite/output/ltac2_check_globalize.v
+++ b/test-suite/output/ltac2_check_globalize.v
@@ -1,5 +1,7 @@
Require Import Ltac2.Ltac2.
+Unset Ltac2 Typed Notations.
+
Ltac2 Notation "foo" := ().
Ltac2 Globalize foo.
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
new file mode 100644
index 0000000000000..5898783ae6d9c
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.out
@@ -0,0 +1,14 @@
+File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
+The command has indeed failed with message:
+This expression has type bool but an expression was expected of type
+constr
+fun (b : bool) =>
+let c := b in
+let (m : '__α Pattern.constr_matching) :=
+ [(Pattern.MatchPattern, pat:(true),
+ (fun _ => fun (_ : constr array) => true));
+ (Pattern.MatchPattern, pat:(false),
+ (fun _ => fun (_ : constr array) => false))] with
+ (t : constr) := c in
+Pattern.one_match0 t m
+:'__α : bool
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
new file mode 100644
index 0000000000000..2de4a96c76cd7
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.v
@@ -0,0 +1,16 @@
+Require Import Ltac2.Ltac2.
+
+Fail Ltac2 foo(b: bool): bool :=
+ let c := b in
+ match! c with
+ | true => true
+ | false => false
+ end.
+(* error used to be on the whole command *)
+
+Ltac2 Globalize fun (b: bool) =>
+ (let c := b in
+ match! c with
+ | true => true
+ | false => false
+ end : bool).
diff --git a/user-contrib/Ltac2/Compat/Coq818.v b/user-contrib/Ltac2/Compat/Coq818.v
index f97a43c0d28c0..d0b4b8576c06e 100644
--- a/user-contrib/Ltac2/Compat/Coq818.v
+++ b/user-contrib/Ltac2/Compat/Coq818.v
@@ -1,5 +1,7 @@
Local Set Warnings "-masking-absolute-name".
+Require Export Ltac2.Compat.Coq819.
+
Require Ltac2.Array.
Module Export Ltac2.
diff --git a/user-contrib/Ltac2/Compat/Coq819.v b/user-contrib/Ltac2/Compat/Coq819.v
new file mode 100644
index 0000000000000..f1345eb96d60f
--- /dev/null
+++ b/user-contrib/Ltac2/Compat/Coq819.v
@@ -0,0 +1,3 @@
+Require Ltac2.Init.
+
+#[export] Unset Ltac2 Typed Notations.