diff options
38 files changed, 292 insertions, 221 deletions
diff --git a/Makefile.doc b/Makefile.doc index 1249555cd7..5aa1ae9850 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -38,10 +38,11 @@ SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)" endif -SPHINXOPTS= -j4 SPHINXWARNERROR ?= 1 ifeq ($(SPHINXWARNERROR),1) -SPHINXOPTS += -W +SPHINXOPTS= -W +else +SPHINXOPTS= endif SPHINXBUILD= sphinx-build SPHINXBUILDDIR= doc/sphinx/_build diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 62e732ce69..c4c6d9bb4f 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = +let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = let open Entries in let nparams = List.length mb.mind_params_ctxt in (* include letins *) let mind_entry_record = match mb.mind_record with @@ -33,39 +33,27 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = inductive types. The set of monomorphic constraints is already part of the graph at that point, but we need to emulate a broken bound variable mechanism for template inductive types. *) - let fold accu ind = match ind.mind_arity with - | RegularArity _ -> accu - | TemplateArity ar -> - match accu with - | None -> Some ar.template_context - | Some ctx -> - (* Ensure that all template contexts agree. This is enforced by the - kernel. *) - let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in - Some ctx - in - let univs = match Array.fold_left fold None mb.mind_packets with + let univs = match mb.mind_template with | None -> ContextSet.empty - | Some ctx -> ctx + | Some ctx -> ctx.template_context in Monomorphic_entry univs | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> - let mind_entry_arity, mind_entry_template = match ind.mind_arity with + let mind_entry_arity = match ind.mind_arity with | RegularArity ar -> let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in ignore ctx; (* we will check that the produced user_arity is equal to the input *) - arity, false + arity | TemplateArity ar -> let ctx = ind.mind_arity_ctxt in let ctx = List.firstn (List.length ctx - nparams) ctx in - Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true + Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level) in { mind_entry_typename = ind.mind_typename; mind_entry_arity; - mind_entry_template; mind_entry_consnames = Array.to_list ind.mind_consnames; mind_entry_lc = Array.map_to_list (fun c -> let ctx, c = Term.decompose_prod_n_assum nparams c in @@ -75,12 +63,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = }) mb.mind_packets in + let check_template ind = match ind.mind_arity with + | RegularArity _ -> false + | TemplateArity _ -> true + in + let mind_entry_template = Array.exists check_template mb.mind_packets in + let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in { mind_entry_record; mind_entry_finite = mb.mind_finite; mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_template; mind_entry_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -89,13 +84,18 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> - List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && - ContextSet.equal template_context ar.template_context && + | TemplateArity ar, TemplateArity {template_level} -> UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false +let check_template ar1 ar2 = match ar1, ar2 with +| None, None -> true +| Some ar, Some {template_context; template_param_levels} -> + List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context +| None, Some _ | Some _, None -> false + let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost @@ -157,10 +157,10 @@ let check_same_record r1 r2 = match r1, r2 with | (NotRecord | FakeRecord | PrimRecord _), _ -> false let check_inductive env mind mb = - let entry = to_entry mind mb in + let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; - mind_universes; mind_variance; mind_sec_variance; + mind_universes; mind_template; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -191,6 +191,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + check "mind_template" (check_template mb.mind_template mind_template); check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) mb.mind_variance mind_variance); check "mind_sec_variance" (Option.is_empty mind_sec_variance); diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli index ac9ea2fb31..9ef6ff017c 100644 --- a/checker/checkTypes.mli +++ b/checker/checkTypes.mli @@ -17,4 +17,4 @@ open Environ (*s Typing functions (not yet tagged as safe) *) val check_polymorphic_arity : - env -> rel_context -> template_arity -> unit + env -> rel_context -> template_universes -> unit diff --git a/checker/values.ml b/checker/values.ml index ed730cff8e..cba96e6636 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -227,8 +227,11 @@ let v_oracle = v_pred v_cst; |] -let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] +let v_template_arity = + v_tuple "template_arity" [|v_univ|] + +let v_template_universes = + v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -265,7 +268,7 @@ let v_mono_ind_arity = v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|] let v_ind_arity = v_sum "inductive_arity" 0 - [|[|v_mono_ind_arity|];[|v_pol_arity|]|] + [|[|v_mono_ind_arity|];[|v_template_arity|]|] let v_one_ind = v_tuple "one_inductive_body" [|v_id; @@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; v_rctxt; v_univs; (* universes *) + Opt v_template_universes; Opt (Array v_variance); Opt (Array v_variance); Opt v_bool; diff --git a/default.nix b/default.nix index ae6a8d06e5..841bccb129 100644 --- a/default.nix +++ b/default.nix @@ -22,7 +22,7 @@ # a symlink to where Coq was installed. { pkgs ? import ./dev/nixpkgs.nix {} -, ocamlPackages ? pkgs.ocamlPackages +, ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_09 , buildIde ? true , buildDoc ? true , doInstallCheck ? true diff --git a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh new file mode 100644 index 0000000000..f8871ae158 --- /dev/null +++ b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then + + elpi_CI_REF="simplify-template" + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + equations_CI_REF="simplify-template" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + paramcoq_CI_REF="simplify-template" + paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq + + mtac2_CI_REF="simplify-template" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + + rewriter_CI_REF="simplify-template" + rewriter_CI_GITURL=https://github.com/ppedrot/rewriter + +fi diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 54baaee1fe..b8a696ef21 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; - sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; + url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; + sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; }) diff --git a/ide/coqide.ml b/ide/coqide.ml index 61e95c21b1..553b834a37 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -244,6 +244,13 @@ let close_and_quit () = List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages; exit 0 +(* Work around a deadlock due to OCaml exit cleanup. The standard [exit] + function calls [flush_all], which can block if one of the opened channels is + not valid anymore. We do not register [at_exit] functions in CoqIDE, so + instead of flushing we simply die as gracefully as possible in the function + below. *) +external sys_exit : int -> 'a = "caml_sys_exit" + let crash_save exitcode = Minilib.log "Starting emergency save of buffers in .crashcoqide files"; let idx = @@ -263,7 +270,7 @@ let crash_save exitcode = in List.iter save_session notebook#pages; Minilib.log "End emergency save"; - exit exitcode + sys_exit exitcode end diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 31dd26d2ba..13ee353c6b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t = t let cook_one_ind ~ntypes - (section_decls,_ as hyps) expmod mip = + hyps expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level;template_context} -> - let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some None - else None) - section_decls - in - let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level;template_context} + | TemplateArity {template_level} -> + TemplateArity {template_level} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in @@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = in Some (Array.append newvariance variance), Some sec_variance in + let mind_template = match mib.mind_template with + | None -> None + | Some {template_param_levels=levels; template_context} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some None + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + Some {template_param_levels=levels; template_context} + in { mind_packets; mind_record; @@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = mind_nparams_rec = mib.mind_nparams_rec + nnewparams; mind_params_ctxt; mind_universes; + mind_template; mind_variance; mind_sec_variance; mind_private = mib.mind_private; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ac130d018d..11a07ee5cf 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -30,8 +30,11 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; +} + +type template_universes = { + template_param_levels : Univ.Level.t option list; template_context : Univ.ContextSet.t; } @@ -218,6 +221,8 @@ type mutual_inductive_body = { mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_template : template_universes option; + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_sec_variance : Univ.Variance.t array option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a3adac7a11..a1122d1279 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -46,9 +46,10 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = + { template_level = Univ.hcons_univ ar.template_level; } + +let hcons_template_universe ar = { template_param_levels = ar.template_param_levels; - (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level; template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function @@ -247,6 +248,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_template = mib.mind_template; mind_variance = mib.mind_variance; mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; @@ -323,6 +325,7 @@ let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_template = Option.Smart.map hcons_template_universe mib.mind_template; mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 8d930b521c..983fa822e9 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; - mind_entry_template : bool; (* Use template polymorphism *) mind_entry_consnames : Id.t list; mind_entry_lc : constr list } @@ -50,6 +49,7 @@ type mutual_inductive_entry = { mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; + mind_entry_template : bool; (* Use template polymorphism *) mind_entry_cumulative : bool; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 501ac99ff3..1b5a77cc96 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env = | TemplateArity _ -> true | RegularArity _ -> false -let template_polymorphic_variables (mind,i) env = - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity { Declarations.template_param_levels = l; _ } -> +let template_polymorphic_variables (mind, _) env = + match (lookup_mind mind env).mind_template with + | Some { Declarations.template_param_levels = l; _ } -> List.map_filter (fun level -> level) l - | RegularArity _ -> [] + | None -> [] let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index cc15109f06..d5aadd0c02 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -101,10 +101,10 @@ let check_indices_matter env_params info indices = else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) -let check_arity env_params env_ar ind = +let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in - let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let ind_min_univ = if template then Some Universe.type0m else None in let univ_info = { ind_squashed=false; ind_has_relevant_arg=false; @@ -200,28 +200,88 @@ let unbounded_from_below u cstrs = let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + (let () = assert (not @@ Univ.Level.is_small l) in true) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in - let univs = - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - in + let univs = Univ.LSet.filter (fun l -> check_level l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> (match Univ.Universe.level u with - | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | Some l -> if Univ.LSet.mem l univs then Some l else None | None -> None) | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in - params, univs + if Universe.is_type0m concl then Some (univs, params) + else if not @@ Univ.LSet.is_empty univs then Some (univs, params) + else None + +let get_param_levels ctx params arity splayed_lc = + let min_univ = match arity with + | RegularArity _ -> + CErrors.user_err + Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.") + | TemplateArity ar -> ar.template_level + in + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + match template_polymorphic_univs ~ctor_levels ctx params min_univ with + | None -> + CErrors.user_err + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + | Some (_, param_levels) -> + param_levels + +let get_template univs params data = + let ctx = match univs with + | Monomorphic ctx -> ctx + | Polymorphic _ -> + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + (* For each type in the block, compute potential template parameters *) + let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in + (* Pick the lower bound of template parameters. Note that in particular, if + one of the the inductive types from the block is Prop-valued, then no + parameters are template. *) + let fold min params = + let map u v = match u, v with + | (None, _) | (_, None) -> None + | Some u, Some v -> + let () = assert (Univ.Level.equal u v) in + Some u + in + List.map2 map min params + in + let params = match params with + | [] -> assert false + | hd :: rem -> List.fold_left fold hd rem + in + { template_param_levels = params; template_context = ctx } -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -237,40 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let arity = match univ_info.ind_min_univ with | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} - | Some min_univ -> - let ctx = match univs with - | Monomorphic ctx -> ctx - | Polymorphic _ -> - CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let ctor_levels = - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - Array.fold_left - (fun levels (d,c) -> - let levels = - List.fold_left (fun levels d -> - Context.Rel.Declaration.fold_constr add_levels d levels) - levels d - in - add_levels c levels) - param_levels - splayed_lc - in - let param_levels, concl_levels = - template_polymorphic_univs ~ctor_levels ctx params min_univ - in - if List.for_all (fun x -> Option.is_empty x) param_levels - && Univ.LSet.is_empty concl_levels then - CErrors.user_err - Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") - else - TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } + | Some min_univ -> TemplateArity { template_level = min_univ; } in let kelim = allowed_sorts univ_info in @@ -285,7 +312,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); - let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + let has_template_poly = mie.mind_entry_template in (* universes *) let env_univs = @@ -306,7 +333,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) - let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) @@ -352,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let data = List.map (abstract_packets usubst) data in + let template = + let check ((arity, _), _, _) = match arity with + | TemplateArity _ -> true + | RegularArity _ -> false + in + if List.exists check data then Some (get_template univs params data) else None + in let env_ar_par = let ctx = Environ.rel_context env_ar_par in @@ -361,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, variance, record, params, Array.of_list data + env_ar_par, univs, template, variance, record, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 723ba5459e..babb82c39e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option -> mutual_inductive_entry -> env * universes + * template_universes option * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context @@ -44,4 +45,4 @@ val template_polymorphic_univs : Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> - Univ.Level.t option list * Univ.LSet.t + (Univ.LSet.t * Univ.Level.t option list) option diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6b8e5265c..58e5e76b61 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env ~sec_univs names prv univs variance +let build_inductive env ~sec_univs names prv univs template variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) @@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_template = template; mind_variance = variance; mind_sec_variance = sec_variance; mind_private = prv; @@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = + let (env_ar_par, univs, template, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env ~sec_univs mie in (* Then check positivity conditions *) @@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env ~sec_univs names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs template variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1be86f2bf8..6325779675 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -185,8 +185,8 @@ let make_subst = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes ctx ar args = - let subst = make_subst (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx (templ, ar) args = + let subst = make_subst (ctx,templ.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes ctx ar paramtyps in + let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b690fe1157..90571844b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : Constr.rel_context -> - template_arity -> param_univs -> Constr.rel_context * Sorts.t - (** {6 Debug} *) type size = Large | Strict diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 535b7de121..a37d04d82c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1303,12 +1303,7 @@ let start_library dir senv = required = senv.required } let export ?except ~output_native_objects senv dir = - let senv = - try join_safe_environment ?except senv - with e -> - let e = Exninfo.capture e in - CErrors.user_err ~hdr:"export" (CErrors.iprint e) - in + let senv = join_safe_environment ?except senv in assert(senv.future_cst = []); let () = check_current_library dir senv in let mp = senv.modpath in diff --git a/lib/control.ml b/lib/control.ml index e67e88ee95..1898eab89e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -75,8 +75,8 @@ let windows_timeout n f x e = if not !exited then begin killed := true; raise Sys.Break end else raise e | e -> - let () = killed := true in let e = Exninfo.capture e in + let () = killed := true in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -201,11 +201,7 @@ let pp_with ft pp = pp_cmd s; pp_close_tag ft () [@warning "-3"] in - try pp_cmd pp - with reraise -> - let reraise = Exninfo.capture reraise in - let () = Format.pp_print_flush ft () in - Exninfo.iraise reraise + pp_cmd pp (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 45fafd2872..7d87fc0220 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -[@@@ocaml.warning "-3"] -let coq_constant s = - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" - Coqlib.init_modules s;; +let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) -let eq = lazy(EConstr.of_constr (coq_constant "eq")) -let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) +let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type")) +let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl")) let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () @@ -369,10 +365,10 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in if not (Stack.is_empty debug_queue) then print_debug_queue true (fst reraise); - Util.iraise reraise + Exninfo.iraise reraise let observe_tac s tac g = if do_observe () @@ -447,14 +443,11 @@ let h_intros l = let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" -let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded") -let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") -let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") - -[@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ - Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" -[@@@ocaml.warning "+3"] +let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded") +let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc") +let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv") + +let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof") let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f7f8004998..9fa0ec8c08 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -47,18 +47,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -[@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ - Coqlib.find_reference "RecursiveDefinition" m s - -let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Coq"; "Arith";"Lt"] +let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref s let coq_init_constant s = - EConstr.of_constr ( - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) -[@@@ocaml.warning "+3"] + EConstr.of_constr(UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s) +;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -122,26 +116,26 @@ let v_id = Id.of_string "v" let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; -let lt = function () -> (coq_init_constant "lt") -[@@@ocaml.warning "-3"] -let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") -let ex = function () -> (coq_init_constant "ex") -let nat = function () -> (coq_init_constant "nat") +let lt = function () -> (coq_init_constant "num.nat.lt") +let le = function () -> Coqlib.lib_ref "num.nat.le" + +let ex = function () -> (coq_init_constant "core.ex.type") +let nat = function () -> (coq_init_constant "num.nat.type") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) -let eq = function () -> (coq_init_constant "eq") +let eq = function () -> (coq_init_constant "core.eq.type") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") -let le_trans = function () -> (coq_constant arith_Nat "le_trans") -let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans") -let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n") -let le_n = function () -> (coq_init_constant "le_n") +let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm") +let le_trans = function () -> (coq_constant "num.nat.le_trans") +let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans") +let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n") +let le_n = function () -> (coq_init_constant "num.nat.le_n") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_O = function () -> (coq_init_constant "O") -let coq_S = function () -> (coq_init_constant "S") -let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") +let coq_O = function () -> (coq_init_constant "num.nat.O") +let coq_S = function () -> (coq_init_constant"num.nat.S") +let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref)) @@ -817,7 +811,7 @@ let rec prove_le g = | App (c, [| x0 ; _ |]) -> EConstr.isVar sigma x0 && Id.equal (destVar sigma x0) (destVar sigma x) && - EConstr.is_global sigma (le ()) c + EConstr.isRefX sigma (le ()) c | _ -> false in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in @@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate = exception EmptySubgoals let build_and_l sigma l = let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in - let conj_constr = Coqlib.build_coq_conj () in + let conj_constr = Coqlib.lib_ref "core.and.conj" in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index f6fbdaa958..fa824a88ee 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -134,7 +134,7 @@ let r_of_rawnum ?loc (sign,n) = | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2)) | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2)))) | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in - Bigint.(sub e (of_int (String.length f))) in + Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in if Bigint.is_strictly_pos e then rmult n (izr (pow10 e)) else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e))) else n (* e = 0 *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aafd662f7d..c9ccd668ca 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a4406aeba1..01994a35c7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let _,scl = splay_arity env sigma conclty in let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = instantiate_universes - env evdref scl ar.template_level (ctx,ar.template_param_levels) in + env evdref scl ar.template_level (ctx,templ.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_constant env (p,u) = diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 7cdfd0637a..a7ba12bb1f 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -120,18 +120,14 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~ let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - entry, status, universes - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = Exninfo.capture reraise in - Exninfo.iraise reraise + let pf, status = by tac pf in + let open Proof_global in + let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + match entries with + | [entry] -> + entry, status, universes + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 2d877bd813..2b14ca7069 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,6 +2,8 @@ : R (-31)%R : R +15e-1%R + : R eq_refl : 102e-2 = 102e-2 : 102e-2 = 102e-2 eq_refl : 102e-1 = 102e-1 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index cb3bce70d4..7be8b18ac8 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -2,6 +2,8 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. +Check 1.5_%R. + Open Scope R_scope. Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 918b0efc5a..8904f3f936 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -41,11 +41,15 @@ Proof. apply Nat.lt_succ_r. Qed. +Register lt_n_Sm_le as num.nat.lt_n_Sm_le. + Theorem le_lt_n_Sm n m : n <= m -> n < S m. Proof. apply Nat.lt_succ_r. Qed. +Register le_lt_n_Sm as num.nat.le_lt_n_Sm. + Hint Immediate lt_le_S: arith. Hint Immediate lt_n_Sm_le: arith. Hint Immediate le_lt_n_Sm: arith. @@ -99,6 +103,8 @@ Proof. apply Nat.succ_lt_mono. Qed. +Register lt_S_n as num.nat.lt_S_n. + Hint Resolve lt_n_Sn lt_S lt_n_S : arith. Hint Immediate lt_S_n : arith. @@ -133,6 +139,8 @@ Notation lt_trans := Nat.lt_trans (only parsing). Notation lt_le_trans := Nat.lt_le_trans (only parsing). Notation le_lt_trans := Nat.le_lt_trans (only parsing). +Register le_lt_trans as num.nat.le_lt_trans. + Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index f12785029a..4657b7f46d 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -764,6 +764,9 @@ Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. Hint Unfold Nat.le : core. Hint Unfold Nat.lt : core. +Register Nat.le_trans as num.nat.le_trans. +Register Nat.nlt_0_r as num.nat.nlt_0_r. + (** [Nat] contains an [order] tactic for natural numbers *) (** Note that [Nat.order] is domain-agnostic: it will not prove diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 1c183930f9..c5a6651c05 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -34,6 +34,8 @@ Proof. intros a. apply (H (S (f a))). auto with arith. Defined. +Register well_founded_ltof as num.nat.well_founded_ltof. + Theorem well_founded_gtof : well_founded gtof. Proof. exact well_founded_ltof. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 149a7a0cc5..beb06ea912 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -159,6 +159,8 @@ Inductive le (n:nat) : nat -> Prop := where "n <= m" := (le n m) : nat_scope. +Register le_n as num.nat.le_n. + Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 998bbc7047..bd5185fdb0 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -32,11 +32,14 @@ Section Well_founded. Inductive Acc (x: A) : Prop := Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. + Register Acc as core.wf.acc. + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. Defined. Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. + Register Acc_inv as core.wf.acc_inv. (** A relation is well-founded if every element is accessible *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index edb03a5c89..718e62b9b7 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl = if not concltemplate then false else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = - IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu - in - not (Univ.LSet.is_empty conclunivs) + Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu | Entries.Polymorphic_entry _ -> false let check_param = function @@ -370,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -385,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames in template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in - let template = match template with + match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); template | None -> should_auto_template indname (template_candidate ()) - in - { mind_entry_typename = indname; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) + ) indnames arities arityconcl constructors in + let is_template = List.for_all (fun t -> t) template in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -409,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; + mind_entry_template = is_template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/record.ml b/vernac/record.ml index 3e44cd85cc..065641989d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,13 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let template = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } + in + let blocks = List.mapi mk_block record_data in + let check_template (id, _, min_univ, _, _, fields, _, _) = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -454,14 +460,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | None, template -> (* auto detect template *) ComInductive.should_auto_template id (template && template_candidate ()) - in - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let blocks = List.mapi mk_block record_data in + let template = List.for_all check_template record_data in let primitive = !primitive_flag && List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data @@ -473,6 +473,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_template = template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e0afb7f483..5d38ea32be 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,28 +92,18 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) let type_vernac opn converted_args ~atts = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then + let depr, callback = vinterp_map opn in + let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts - with - | reraise -> - let reraise = Exninfo.capture reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - Exninfo.iraise reraise + in + let hunk = callback converted_args in + hunk ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 59557a60a6..280343f315 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -18,12 +18,9 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; - Flags.with_option Flags.we_are_parsing (fun () -> - try Pcoq.Entry.parse entry pa - with e when CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in - Exninfo.iraise (e, info)) - () + Flags.with_option Flags.we_are_parsing + (fun () -> Pcoq.Entry.parse entry pa) + () end |