diff options
34 files changed, 229 insertions, 100 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 59a85e4726..9cb7a65ab5 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -6,4 +6,6 @@ ci_dir="$(dirname "$0")" git_download compcert ( cd "${CI_BUILD_DIR}/compcert" && \ - ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) + ./configure -ignore-coq-version x86_32-linux && \ + make && \ + make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)') diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 169d1a41db..4a332406a2 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")" git_download vst +export COMPCERT=bundled + ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst new file mode 100644 index 0000000000..ab8768a079 --- /dev/null +++ b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Printing bug with notations for n-ary applications used with applied references. + (`#12683 <https://github.com/coq/coq/pull/12683>`_, + fixes `#12682 <https://github.com/coq/coq/pull/12682>`_, + by Hugo Herbelin). diff --git a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst new file mode 100644 index 0000000000..4df8e97e34 --- /dev/null +++ b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Do not store the full environment inside ssr ast_closure_term + (`#12708 <https://github.com/coq/coq/pull/12708>`_, + fixes `#12707 <https://github.com/coq/coq/issues/12707>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst new file mode 100644 index 0000000000..c654ddd69d --- /dev/null +++ b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Properly report the mismatched magic number of vo files + (`#12677 <https://github.com/coq/coq/pull/12677>`_, + fixes `#12513 <https://github.com/coq/coq/issues/12513>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e5c2056c40..d4707a04d8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -14,9 +14,9 @@ Version 8.12 Summary of changes ~~~~~~~~~~~~~~~~~~ -|Coq| version 8.12 integrates many quality-of-life improvements, +|Coq| version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, -along with many bug-fixes and major improvements to the reference manual. +along with many bug fixes and major improvements to the reference manual. The main changes include: - New :ref:`binder notation<812Implicit>` for non-maximal implicit arguments using :g:`[ ]` @@ -64,6 +64,23 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. +Previously, most components of Coq had a single principal maintainer. +This was changed in 8.12 (`#11295 +<https://github.com/coq/coq/pull/11295>`_) so that every component now has +a team of maintainers, who are in charge of reviewing and +merging incoming pull requests. This gave us a chance to +significantly expand the pool of maintainters and provide faster +feedback to contributors. Special thanks to all our maintainers! + +Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej +Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, +Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, +Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond, +Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent +Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico +Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann + The 59 contributors to this version are Abhishek Anand, Yves Bertot, Frédéric Besson, Lasse Blaauwbroek, Simon Boulier, Quentin Carbonneaux, Tej Chajed, Arthur Charguéraud, Cyril Cohen, Pierre Courtieu, Matthew Dempsky, Maxime Dénès, @@ -72,8 +89,8 @@ Jesús Gallego Arias, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel Gruetter, Attila Gáspár, Hugo Herbelin, Jan-Oliver Kaiser, Robbert Krebbers, Vincent Laporte, Olivier Laurent, Xavier Leroy, Thomas Letan, Yishuai Li, Kenji Maillard, Erik Martin-Dorel, Guillaume Melquiond, Ike Mulder, -Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Clément -Pit-Claudel, Pierre-Marie Pédrot, Ramkumar Ramachandra, Lars Rasmusson, Daniel +Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Pierre-Marie +Pédrot, Clément Pit-Claudel, Ramkumar Ramachandra, Lars Rasmusson, Daniel de Rauglaudre, Talia Ringer, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, @scinart, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia, diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index d6951fff6d..83c158e057 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -1548,12 +1548,21 @@ module Parsable = struct Stream.Failure -> let loc = get_loc () in restore (); - Ploc.raise loc (Stream.Error ("illegal begin of " ^ entry.ename)) + Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename)) | Stream.Error _ as exc -> - let loc = get_loc () in restore (); Ploc.raise loc exc + let loc = get_loc () in restore (); + Loc.raise ~loc exc | exc -> + let exc,info = Exninfo.capture exc in let loc = Stream.count cs, Stream.count cs + 1 in - restore (); Ploc.raise (Ploc.make_unlined loc) exc + restore (); + (* If the original exn had a loc, keep it *) + let info = + match Loc.get_loc info with + | Some _ -> info + | None -> Loc.add_loc info (Ploc.make_unlined loc) + in + Exninfo.iraise (exc,info) let parse_parsable e p = L.State.set !(p.lexer_state); @@ -1561,11 +1570,10 @@ module Parsable = struct let c = parse_parsable e p in p.lexer_state := L.State.get (); c - with Ploc.Exc (loc,e) -> + with exn -> + let exn,info = Exninfo.capture exn in L.State.drop (); - let loc' = Loc.get_loc (Exninfo.info e) in - let loc = match loc' with None -> loc | Some loc -> loc in - Loc.raise ~loc e + Exninfo.iraise (exn,info) let make ?loc cs = let lexer_state = ref (L.State.init ()) in diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index 056a2b7ad3..e121342c94 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -16,10 +16,3 @@ let dummy = let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} - -exception Exc of Loc.t * exn - -let raise loc exc = - match exc with - Exc (_, _) -> raise exc - | _ -> raise (Exc (loc, exc)) diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index 15a5a74455..4b865110c3 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -2,20 +2,6 @@ (* ploc.mli,v *) (* Copyright (c) INRIA 2007-2017 *) -(* located exceptions *) - -exception Exc of Loc.t * exn - (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with - the input location [loc]. To be used to specify a location - for an error. This exception must not be raised by [raise] but - rather by [Ploc.raise] (see below), to prevent the risk of several - encapsulations of [Ploc.Exc]. *) - -val raise : Loc.t -> exn -> 'a - (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc], - re-raise it (ignoring the new location [loc]), else raise the - exception [Ploc.Exc loc e]. *) - val make_unlined : int * int -> Loc.t (** [Ploc.make_unlined] is like [Ploc.make] except that the line number is not provided (to be used e.g. when the line number is unknown. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 95df626d4c..3667757a2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r = insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = + (* This is to ensure that notations for coercions are used only when + the coercion is fully applied; not explicitly done yet, but we + could also expect that the notation is exactly talking about the + coercion *) match nargs with | None -> l | Some nargs -> - List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l + List.filter (fun (keyrule,pat,n as _rule) -> + match n with + | AppBoundedNotation n -> n > nargs + | AppUnboundedNotation | NotAppNotation -> false) l (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [], [] in (* Adjust to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match n with - | Some n when nallargs >= n -> + | AppBoundedNotation n when nallargs >= n -> let args1, args2 = List.chop n args in let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in let args2impls = @@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules = [] else try List.skipn n argsimpls with Failure _ -> [] in DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls - | None -> + | AppUnboundedNotation -> t, [], [], [] + | NotAppNotation -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | _ -> raise No_match in + | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 987aa63392..6d4ab8b4d6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv = | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = - if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in - List.rev_append pars pl in + List.rev_append pars pl + in let (_,argscs) = find_remaining_scopes [] pl head in let pats = List.map2 (in_pat_sc scopes) argscs pl in - DAst.make ?loc @@ RCPatCstr(head, [], pats) + DAst.make ?loc @@ RCPatCstr(head, pats, []) end | CPatCstr (head, None, pl) -> begin diff --git a/interp/notation.ml b/interp/notation.ml index e282d62396..c4e9496b95 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -type notation_rule = interp_rule * interpretation * int option +type notation_applicative_status = + | AppBoundedNotation of int + | AppUnboundedNotation + | NotAppNotation + +type notation_rule = interp_rule * interpretation * notation_applicative_status let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in @@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) - | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args) | NList (_,_,NApp (NRef ref,args),_,_) | NBinderList (_,_,NApp (NRef ref,args),_,_) -> - RefKey (canonical_gr ref), Some (List.length args) - | NRef ref -> RefKey(canonical_gr ref), None - | NApp (_,args) -> Oth, Some (List.length args) - | _ -> Oth, None + RefKey (canonical_gr ref), AppBoundedNotation (List.length args) + | NRef ref -> RefKey(canonical_gr ref), NotAppNotation + | NApp (_,args) -> Oth, AppBoundedNotation (List.length args) + | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation + | _ -> Oth, NotAppNotation (** Dealing with precedences *) diff --git a/interp/notation.mli b/interp/notation.mli index c39bfa6e28..05ddd25a62 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_applicative_status = + | AppBoundedNotation of int + | AppUnboundedNotation + | NotAppNotation + +type notation_rule = interp_rule * interpretation * notation_applicative_status (** Return the possible notations for a given term *) val uninterp_notations : 'a glob_constr_g -> notation_rule list diff --git a/lib/objFile.ml b/lib/objFile.ml index 96db51a010..26367aaffa 100644 --- a/lib/objFile.ml +++ b/lib/objFile.ml @@ -182,7 +182,7 @@ let open_in ~file = let version = input_int32 ch in let () = if not (Int32.equal magic magic_number) then - let e = { filename = file; actual = version; expected = magic_number } in + let e = { filename = file; actual = magic; expected = magic_number } in raise (Bad_magic_number e) in let () = diff --git a/lib/system.ml b/lib/system.ml index e25f758865..1aadaf6d3a 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -239,9 +239,12 @@ let intern_state magic filename = let with_magic_number_check f a = try f a with - | Bad_magic_number {filename=fname; _} -> + | Bad_magic_number {filename=fname; actual; expected} -> CErrors.user_err ~hdr:"with_magic_number_check" - (str"File " ++ str fname ++ strbrk" is corrupted.") + (str"File " ++ str fname ++ strbrk" has bad magic number " ++ + (str @@ Int32.to_string actual) ++ str" (expected " ++ (str @@ Int32.to_string expected) ++ str")." ++ + spc () ++ + strbrk "It is corrupted or was compiled with another version of Coq.") | Bad_version_number {filename=fname;actual=actual;expected=expected} -> CErrors.user_err ~hdr:"with_magic_number_check" (str"File " ++ str fname ++ strbrk" has bad version number " ++ diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 8adffdc709..f6a741f468 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -51,13 +51,19 @@ type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) +type ast_glob_env = { + ast_ltacvars : Id.Set.t; + ast_extra : Genintern.Store.t; + ast_intern_sign : Genintern.intern_variable_status; +} + (* These terms are raw but closed with the intenalization/interpretation * context. It is up to the tactic receiving it to decide if such contexts * are useful or not, and eventually manipulate the term before turning it * into a constr *) type ast_closure_term = { body : Constrexpr.constr_expr; - glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *) + glob_env : ast_glob_env option; (* for Tacintern.intern_constr *) interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *) annotation : [ `None | `Parens | `DoubleParens | `At ]; } diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 65204b7868..1b7768852e 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -302,6 +302,11 @@ let mk_ast_closure_term a t = { } let glob_ast_closure_term (ist : Genintern.glob_sign) t = + let ist = { + ast_ltacvars = ist.Genintern.ltacvars; + ast_intern_sign = ist.Genintern.intern_sign; + ast_extra = ist.Genintern.extra; + } in { t with glob_env = Some ist } let subst_ast_closure_term (_s : Mod_subst.substitution) t = (* _s makes sense only for glob constr *) @@ -1124,8 +1129,7 @@ let tclDO n tac = let _, info = Exninfo.capture e in let e' = CErrors.UserError (l, prefix i ++ s) in Exninfo.iraise (e', info) - | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a12b4aad11..1c81fbc10b 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -490,7 +490,6 @@ let equality_inj l b id c = let msg = ref "" in try Proofview.V82.of_tactic (Equality.inj None l b None c) gl with - | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s)) | CErrors.UserError (_,s) when msg := Pp.string_of_ppcmds s; !msg = "Not a projectable equality but a discriminable one." || diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index ad0a31622c..d99ead139d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -150,7 +150,15 @@ let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } = let sigma = sigma goal in let ist = Ssrcommon.option_assert_get glob_env (Pp.str"not a term") in (* We use the env of the goal, not the global one *) - let ist = { ist with Genintern.genv } in + let ist = + let open Genintern in + { + ltacvars = ist.ast_ltacvars; + extra = ist.ast_extra; + intern_sign = ist.ast_intern_sign; + genv; + } + in (* We open extra_scope *) let body = match extra_scope with diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 400acc25b6..2feae8cc25 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1334,6 +1334,12 @@ let thin_evars env sigma sign c = let c' = applyrec (env,0) c in (!sigma, c') +exception NotFoundInstance of exn +let () = CErrors.register_handler (function + | NotFoundInstance e -> + Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e) + | _ -> None) + let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in @@ -1478,7 +1484,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) - with e -> user_err (Pp.str "Cannot find an instance") + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + Exninfo.iraise (NotFoundInstance e, info) else ((if debug_ho_unification () then let evi = Evd.find evd evk in diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 414663c826..207ffc7b86 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -66,6 +66,7 @@ exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function | CErrors.UserError _ | TypeError _ | PretypeError _ + | Reductionops.AnomalyInConversion _ | Nametab.GlobalizationError _ -> true | _ -> false diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 07154d4e03..c31ecc135c 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,8 +1,8 @@ Geninterp Locus Locusops -Pretype_errors Reductionops +Pretype_errors Inductiveops Arguments_renaming Retyping diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 594b8ab54c..fdc770dba6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1085,12 +1085,25 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV +(* NOTE: We absorb anomalies happening in the conversion tactic, which + is a bit ugly. This is mostly due to efficiency both in tactics and + in the conversion machinery itself. It is not uncommon for a tactic + to send some ill-typed term to the engine. + + We would usually say that a tactic that converts ill-typed terms is + buggy, but fixing the tactic could have a very large runtime cost + *) +exception AnomalyInConversion of exn + +let _ = CErrors.register_handler (function + | AnomalyInConversion e -> + Some Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) + | _ -> None) + let report_anomaly (e, info) = let e = - if is_anomaly e then - let msg = Pp.(str "Conversion test raised an anomaly:" ++ - spc () ++ CErrors.print e) in - UserError (None, msg) + if is_anomaly e then AnomalyInConversion e else e in Exninfo.iraise (e, info) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 218936edfb..0f288cdd46 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -283,3 +283,5 @@ val whd_betaiota_deltazeta_for_iota_state : (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr + +exception AnomalyInConversion of exn diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 82ce2234e3..63cafbf76d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -236,7 +236,7 @@ let with_prods nprods h f = f gl (h, diff) with e when CErrors.noncritical e -> let e, info = Exninfo.capture e in - Tacticals.New.tclZEROMSG ~info (CErrors.print e) end + Proofview.tclZERO ~info e end else Proofview.Goal.enter begin fun gl -> if Int.equal nprods 0 then f gl (h, None) diff --git a/test-suite/bugs/closed/bug_12534.v b/test-suite/bugs/closed/bug_12534.v new file mode 100644 index 0000000000..a55515feb6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12534.v @@ -0,0 +1,9 @@ +Record C {PROP: Prop} (P : PROP) : Type := { c : unit}. +Check fun '{|c:=x|} => tt. (* Fine *) +Arguments Build_C {_ _} _. +Check fun '(Build_C _) => tt. (* Works. Note: just 1 argument! *) +Check fun '{|c:=x|} => tt. +(* Error: The constructor @Build_C (in type @C) expects 1 argument. *) + +Set Asymmetric Patterns. +Check fun '{|c:=x|} => tt. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 53ad8a9612..90a6a2ad96 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -80,6 +80,12 @@ NIL : list nat : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z +{|fun x : Z => x + x; 0|} + : Z +{|op; 0; 1|} + : Z +false = 0 + : Prop Init.Nat.add : nat -> nat -> nat S diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 7d2f1e9ba8..d0b2f40f9c 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|]. (**********************************************************************) (* Test recursive notations involving applications *) -(* Caveat: does not work for applied constant because constants are *) -(* classified as notations for the particular constant while this *) -(* generic application notation is classified as generic *) + +Module Application. Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). + +(* Application to a variable *) + Check fun f => {| f; 0; 1; 2 |} : Z. +(* Application to a fun *) + +Check {| (fun x => x+x); 0 |}. + +(* Application to a reference *) + +Axiom op : Z -> Z -> Z. +Check {| op; 0; 1 |}. + +(* Interaction with coercion *) + +Axiom c : Z -> bool. +Coercion c : Z >-> bool. +Check false = {| c; 0 |}. + +End Application. + (**********************************************************************) (* Check printing of notations from other modules *) diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index a2d7013dfa..b346b3ee5c 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -88,7 +88,8 @@ let inj_wit ?loc wit x = let of_variable {loc;v=id} = let qid = Libnames.qualid_of_ident ?loc id in if Tac2env.is_constructor qid then - CErrors.user_err ?loc (str "Invalid identifier") + CErrors.user_err ?loc (str "Invalid identifier" ++ spc () ++ Id.print id ++ + spc () ++ str "classifying as an Ltac2 constructor") else CAst.make ?loc @@ CTacRef (RelId qid) let of_anti f = function @@ -229,15 +230,19 @@ let pattern_vars pat = let rec aux () accu pat = match pat.CAst.v with | Constrexpr.CPatVar id | Constrexpr.CEvar (id, []) -> - let () = check_pattern_id ?loc:pat.CAst.loc id in - Id.Set.add id accu + let loc = pat.CAst.loc in + let () = check_pattern_id ?loc id in + Id.Map.add id loc accu | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat in - aux () Id.Set.empty pat + aux () Id.Map.empty pat let abstract_vars loc ?typ vars tac = - let get_name = function Name id -> Some id | Anonymous -> None in + let get_name na = match na.CAst.v with + | Name id -> Some (CAst.make ?loc:na.CAst.loc id) + | Anonymous -> None + in let def = try Some (List.find_map get_name vars) with Not_found -> None in let na, tac = match def with | None -> (Anonymous, tac) @@ -245,18 +250,18 @@ let abstract_vars loc ?typ vars tac = (* Trick: in order not to shadow a variable nor to choose an arbitrary name, we reuse one which is going to be shadowed by the matched variables anyways. *) - let build_bindings (n, accu) na = match na with + let build_bindings (n, accu) { CAst.loc; CAst.v = na } = match na with | Anonymous -> (n + 1, accu) | Name _ -> let get = global_ref ?loc (kername array_prefix "get") in - let args = [of_variable CAst.(make ?loc id0); of_int CAst.(make ?loc n)] in + let args = [of_variable id0; of_int CAst.(make ?loc n)] in let e = CAst.make ?loc @@ CTacApp (get, args) in let accu = (CAst.make ?loc @@ CPatVar na, e) :: accu in (n + 1, accu) in let (_, bnd) = List.fold_left build_bindings (0, []) vars in let tac = CAst.make ?loc @@ CTacLet (false, bnd, tac) in - (Name id0, tac) + (Name id0.CAst.v, tac) in let pat = CAst.make ?loc @@ CPatVar na in let pat = match typ with @@ -281,7 +286,7 @@ let of_conversion {loc;v=c} = match c with let pat = of_option ?loc of_pattern (Some pat) in let c = of_constr c in (* Order is critical here *) - let vars = List.map (fun id -> Name id) (Id.Set.elements vars) in + let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) (Id.Map.bindings vars) in let c = abstract_vars loc vars c in of_tuple [pat; c] @@ -406,8 +411,8 @@ let of_constr_matching {loc;v=m} = in let vars = pattern_vars pat in (* Order of elements is crucial here! *) - let vars = Id.Set.elements vars in - let vars = List.map (fun id -> Name id) vars in + let vars = Id.Map.bindings vars in + let vars = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in (* Annotate the bound array variable with constr type *) let typ = let t_constr = coq_core "constr" in @@ -428,11 +433,11 @@ let of_goal_matching {loc;v=gm} = let mk_pat {loc;v=p} = match p with | QConstrMatchPattern pat -> let knd = constructor ?loc (pattern_core "MatchPattern") [] in - (Anonymous, pat, knd) + (CAst.make ?loc Anonymous, pat, knd) | QConstrMatchContext (id, pat) -> let na = extract_name ?loc id in let knd = constructor ?loc (pattern_core "MatchContext") [] in - (na, pat, knd) + (CAst.make ?loc na, pat, knd) in let mk_gpat {loc;v=p} = let concl_pat = p.q_goal_match_concl in @@ -442,23 +447,22 @@ let of_goal_matching {loc;v=gm} = let map accu (na, pat) = let (ctx, pat, knd) = mk_pat pat in let vars = pattern_vars pat in - (Id.Set.union vars accu, (na, ctx, pat, knd)) + (Id.Map.fold Id.Map.add vars accu, (na, ctx, pat, knd)) in let (vars, hyps_pats) = List.fold_left_map map vars hyps_pats in let map (_, _, pat, knd) = of_tuple [knd; of_pattern pat] in let concl = of_tuple [concl_knd; of_pattern concl_pat] in let r = of_tuple [of_list ?loc map hyps_pats; concl] in - let hyps = List.map (fun ({CAst.v=na}, _, _, _) -> na) hyps_pats in - let map (_, na, _, _) = na in - let hctx = List.map map hyps_pats in + let hyps = List.map (fun (na, _, _, _) -> na) hyps_pats in + let hctx = List.map (fun (_, na, _, _) -> na) hyps_pats in (* Order of elements is crucial here! *) - let vars = Id.Set.elements vars in - let subst = List.map (fun id -> Name id) vars in + let vars = Id.Map.bindings vars in + let subst = List.map (fun (id, loc) -> CAst.make ?loc (Name id)) vars in (r, hyps, hctx, subst, concl_ctx) in let map {loc;v=(pat, tac)} = let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in - let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx], tac) in + let tac = CAst.make ?loc @@ CTacFun ([CAst.make ?loc @@ CPatVar cctx.CAst.v], tac) in let tac = abstract_vars loc subst tac in let tac = abstract_vars loc hctx tac in let tac = abstract_vars loc hyps tac in diff --git a/vernac/declare.ml b/vernac/declare.ml index df75e121d8..12a261517f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -535,10 +535,13 @@ module Internal = struct ; proof_entry_type = Some typ }, args - type nonrec constant_obj = constant_obj + module Constant = struct + type t = constant_obj + let tag = objConstant + let kind obj = obj.cst_kind + end let objVariable = objVariable - let objConstant = objConstant end diff --git a/vernac/declare.mli b/vernac/declare.mli index adb5bd026f..c5a8afbad5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -556,9 +556,13 @@ end module Internal : sig - type constant_obj + (* Liboject exports *) + module Constant : sig + type t + val tag : t Libobject.Dyn.tag + val kind : t -> Decls.logical_kind + end - val objConstant : constant_obj Libobject.Dyn.tag val objVariable : unit Libobject.Dyn.tag end diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e0974ac027..b93c920654 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1331,10 +1331,8 @@ let pr_vernac_attributes = | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () let pr_vernac ({v = {control; attrs; expr}} as v) = - try - tag_vernac v - (pr_vernac_control control ++ - pr_vernac_attributes attrs ++ - pr_vernac_expr expr ++ - sep_end expr) - with e -> CErrors.print e + tag_vernac v + (pr_vernac_control control ++ + pr_vernac_attributes attrs ++ + pr_vernac_expr expr ++ + sep_end expr) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 176ddd6c5b..2b46542287 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -688,7 +688,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) = constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) end @@ - DynHandle.add Declare.Internal.objConstant begin fun _ -> + DynHandle.add Declare.Internal.Constant.tag begin fun _ -> Some (print_constant with_values sep (Constant.make1 kn) None) end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> @@ -796,7 +796,7 @@ let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let handler = - DynHandleF.add Declare.Internal.objConstant begin fun _ -> + DynHandleF.add Declare.Internal.Constant.tag begin fun _ -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in let typ = cb.const_type in diff --git a/vernac/search.ml b/vernac/search.ml index 2a21184c1e..abefeab779 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -79,11 +79,11 @@ let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> co let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> let handler = - DynHandle.add Declare.Internal.objConstant begin fun _ -> + DynHandle.add Declare.Internal.Constant.tag begin fun obj -> let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in - let kind = Dumpglob.constant_kind cst in + let kind = Declare.Internal.Constant.kind obj in fn gr (Some kind) env typ end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> |