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.