From 9f6e238fac96a123e7cb2bb2b2caec104bc4b916 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 18 Aug 2019 19:46:50 +0200 Subject: Declare universes for variables outside of Declare.declare_variable (letins still declare universes in declare_variable as they use entries) The section check_same_poly is moved to declare_universe_context (it makes more sense there, universe polymorphism doesn't apply to the variables/letins themselves) --- vernac/comAssumption.ml | 3 ++- vernac/lemmas.ml | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e3f90ab98c..f6debd8777 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -50,7 +50,8 @@ match scope with | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in let kind = Decls.IsAssumption kind in - let decl = SectionLocalAssum {typ; univs; poly; impl} in + let () = Declare.declare_universe_context ~poly univs in + let decl = SectionLocalAssum {typ; impl} in let () = declare_variable ~name ~kind decl in let () = assumption_message name in let r = GlobRef.VarRef name in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 42d1a1f3fc..b4875bbdd2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -265,7 +265,8 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect Univ.ContextSet.of_context univs | Monomorphic_entry univs -> univs in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_universe_context ~poly univs in + let c = Declare.SectionLocalAssum {typ=t_i; impl} in let () = Declare.declare_variable ~name ~kind c in GlobRef.VarRef name, impargs | Global local -> -- cgit v1.2.3 From 5685e37442e49ce77831a371c471716c3ccb0a2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 18 Aug 2019 21:18:18 +0200 Subject: Move do_primitive from comassumption to its own module. Primitives don't have anything to do with assumptions. --- vernac/comAssumption.ml | 27 --------------------------- vernac/comAssumption.mli | 2 -- vernac/comPrimitive.ml | 37 +++++++++++++++++++++++++++++++++++++ vernac/comPrimitive.mli | 11 +++++++++++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 2 +- 6 files changed, 50 insertions(+), 30 deletions(-) create mode 100644 vernac/comPrimitive.ml create mode 100644 vernac/comPrimitive.mli (limited to 'vernac') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f6debd8777..a56cf9ab9a 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -190,33 +190,6 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = in () -let do_primitive id prim typopt = - if Lib.sections_are_opened () then - CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); - if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; - let env = Global.env () in - let evd = Evd.from_env env in - let evd, typopt = Option.fold_left_map - (interp_type_evars_impls ~impls:empty_internalization_env env) - evd typopt - in - let evd = Evd.minimize_universes evd in - let uvars, impls, typopt = match typopt with - | None -> Univ.LSet.empty, [], None - | Some (ty,impls) -> - EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) - in - let evd = Evd.restrict_universe_context evd uvars in - let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in - let entry = { prim_entry_type = typopt; - prim_entry_univs = uctx; - prim_entry_content = prim; - } - in - let _kn : Names.Constant.t = - declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (PrimitiveEntry entry) in - Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared") - let named_of_rel_context l = let open EConstr.Vars in let open RelDecl in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 2715bd8305..44db47e1cc 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -47,5 +47,3 @@ val context : poly:bool -> local_binder_expr list -> unit - -val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml new file mode 100644 index 0000000000..06fafddafb --- /dev/null +++ b/vernac/comPrimitive.ml @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Univ.LSet.empty, [], None + | Some (ty,impls) -> + EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty) + in + let evd = Evd.restrict_universe_context evd uvars in + let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in + let entry = Entries.{ + prim_entry_type = typopt; + prim_entry_univs = uctx; + prim_entry_content = prim; + } + in + let _kn : Names.Constant.t = + Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in + Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared") diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli new file mode 100644 index 0000000000..c0db1cc464 --- /dev/null +++ b/vernac/comPrimitive.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 4868182bb3..d9d993f5b5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -26,6 +26,7 @@ Indschemes Obligations ComDefinition Classes +ComPrimitive ComAssumption ComInductive ComFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bc47ad8699..87abb9da59 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2607,7 +2607,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacPrimitive (id, prim, typopt) -> VtDefault(fun () -> unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt) + ComPrimitive.do_primitive id prim typopt) | VernacComments l -> VtDefault(fun () -> unsupported_attributes atts; -- cgit v1.2.3 From 2cdccb3f050b68fdfa36ab1ac444b7507564cb77 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 19 Aug 2019 16:15:40 +0200 Subject: Cleanup ComAssumption The general idea is to move tests on scope=Discharge and on Lib.sections_are_opened up in the call stack. This allows better control over the universe manipulation. There are some corner case behaviour change, eg: - [Context (foo:=bla)] outside a section correctly declares an axiom (fix #10668) - (not observable) universes for [Variable A B : Type] in section are declared only once - universes and universe names for [Axiom A B : Type] are declared only once. This changes the qualification of the universe name: before it was the last axiom (so [B.u0]), now it's the first one ([A.u0]). Probably nobody cares about this. - context outside section uses different [kind] I'm not sure why context outside a section behaves differently based on whether we're in a module type, I tried to preserve it but maybe we should uniformize. The universe manipulation for Axiom (in the declare_assumptions function) is a bit awkward, maybe when there are multiple monomorphic axioms instead of trying to attach the universes to the first one we should just declare them separately like with Context. OTOH unlike with context dropping the universe names seems incorrect. --- vernac/comAssumption.ml | 258 +++++++++++++++++++++++++---------------------- vernac/comAssumption.mli | 37 +++++-- 2 files changed, 166 insertions(+), 129 deletions(-) (limited to 'vernac') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a56cf9ab9a..42c6250919 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -11,7 +11,6 @@ open CErrors open Util open Vars -open Declare open Names open Context open Constrexpr_ops @@ -41,28 +40,20 @@ let should_axiom_into_instance = let open Decls in function true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=name} = -let open DeclareDef in -match scope with -| Discharge -> - let univs = match univs with - | Monomorphic_entry univs -> univs - | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs - in +let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in - let () = Declare.declare_universe_context ~poly univs in - let decl = SectionLocalAssum {typ; impl} in - let () = declare_variable ~name ~kind decl in - let () = assumption_message name in + let decl = Declare.SectionLocalAssum {typ; impl} in + let () = Declare.declare_variable ~name ~kind decl in + let () = Declare.assumption_message name in let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in - (r,Univ.Instance.empty) + () -| Global local -> +let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with | NoInline -> None @@ -71,15 +62,18 @@ match scope with in let kind = Decls.IsAssumption kind in let decl = Declare.ParameterEntry (None,(typ,univs),inl) in - let kn = declare_constant ~name ~local ~kind decl in + let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in - let () = assumption_message name in + let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in - let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in + let local = match local with + | Declare.ImportNeedQualified -> true + | Declare.ImportDefaultBehavior -> false + in let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in let inst = match univs with | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs @@ -91,22 +85,45 @@ let interp_assumption ~program_mode sigma env impls c = let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in sigma, (ty, impls) -(* When monomorphic the universe constraints are declared with the first declaration only. *) -let next_uctx = - let empty_uctx = Monomorphic_entry Univ.ContextSet.empty in +(* When monomorphic the universe constraints and universe names are + declared with the first declaration only. *) +let next_univs = + let empty_univs = Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in function - | Polymorphic_entry _ as uctx -> uctx - | Monomorphic_entry _ -> empty_uctx + | Polymorphic_entry _, _ as univs -> univs + | Monomorphic_entry _, _ -> empty_univs -let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = - let refs, _ = - List.fold_left (fun (refs,uctx) id -> - let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in - ref::refs, next_uctx uctx) - ([],uctx) idl - in - List.rev refs +let context_set_of_entry = function + | Polymorphic_entry (_,uctx) -> Univ.ContextSet.of_context uctx + | Monomorphic_entry uctx -> uctx +let declare_assumptions ~poly ~scope ~kind univs nl l = + let open DeclareDef in + let () = match scope with + | Discharge -> + (* declare universes separately for variables *) + Declare.declare_universe_context ~poly (context_set_of_entry (fst univs)) + | Global _ -> () + in + let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) -> + (* NB: here univs are ignored when scope=Discharge *) + let typ = replace_vars subst typ in + let univs,subst' = + List.fold_left_map (fun univs id -> + let refu = match scope with + | Discharge -> + declare_variable is_coe ~kind typ imps Glob_term.Explicit id; + GlobRef.VarRef id.CAst.v, Univ.Instance.empty + | Global local -> + declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id + in + next_univs univs, (id.CAst.v, Constr.mkRef refu)) + univs idl + in + subst'@subst, next_univs univs) + ([], univs) l + in + () let maybe_error_many_udecls = function | ({CAst.loc;v=id}, Some _) -> @@ -176,112 +193,113 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = IMO, thus I think we should adapt `prepare_parameter` to handle this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in - let uctx = Evd.check_univ_decl ~poly sigma udecl in + let univs = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in - let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) -> - let typ = replace_vars subst typ in - let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in - let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) - idl refs - in - subst'@subst, next_uctx uctx) - ([], uctx) l - in - () + declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l let named_of_rel_context l = - let open EConstr.Vars in - let open RelDecl in let acc, ctx = List.fold_right (fun decl (subst, ctx) -> - let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in - let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in - (EConstr.mkVar id :: subst, d :: ctx)) + let d = RelDecl.(to_tuple (map_constr (EConstr.Vars.substl subst) decl)) in + let id, _, _ as d = on_pi1 (fun annot -> + match binder_name annot with + | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") + | Name id -> id) + d + in + (EConstr.mkVar id :: subst, d :: ctx)) l ([], []) in ctx +let context_insection sigma ~poly ctx = + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + let fn = function + | name, None, t, impl -> + let kind = Decls.Context in + declare_variable false ~kind t [] impl (CAst.make name) + | name, Some b, t, impl -> + (* We need to get poly right for check_same_poly *) + let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + in + let entry = Declare.definition_entry ~univs ~types:t b in + let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge + ~kind:Decls.Definition UnivNames.empty_binders entry [] + in + () + in + List.iter fn ctx + +let context_nosection sigma ~poly ctx = + let univs = + match ctx, poly with + | [_], _ | _, true -> Evd.univ_entry ~poly sigma + | _, false -> + (* Multiple monomorphic axioms: declare universes separately to + avoid redeclaring them. *) + let uctx = Evd.universe_context_set sigma in + let () = Declare.declare_universe_context ~poly uctx in + Monomorphic_entry Univ.ContextSet.empty + in + let fn (name,b,t,_impl) = + let kind = Decls.(IsAssumption Logical) in + let decl = match b with + | None -> + Declare.ParameterEntry (None,(t,univs),None) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + Declare.DefinitionEntry entry + in + (* let local = Declare.ImportNeedQualified in *) + let cst = Declare.declare_constant ~name ~kind ~local:Declare.ImportNeedQualified decl in + let () = Declare.assumption_message name in + let env = Global.env () in + (* why local when is_modtype? *) + let () = if Lib.is_modtype() || Option.is_empty b then + Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst) + in + () + in + List.iter fn ctx + let context ~poly l = let env = Global.env() in let sigma = Evd.from_env env in - let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in + let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in - let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in - let ctx = - try named_of_rel_context fullctx - with e when CErrors.noncritical e -> - user_err Pp.(str "Anonymous variables not allowed in contexts.") - in - let univs = - match ctx with - | [] -> assert false - | [_] -> Evd.univ_entry ~poly sigma - | _::_::_ -> - if Lib.sections_are_opened () - then - (* More than 1 variable in a section: we can't associate - universes to any specific variable so we declare them - separately. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - if poly then Polymorphic_entry ([||], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - end - else if poly then - (* Multiple polymorphic axioms: they are all polymorphic the same way. *) - Evd.univ_entry ~poly sigma - else - (* Multiple monomorphic axioms: declare universes separately - to avoid redeclaring them. *) - begin - let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context ~poly uctx; - Monomorphic_entry Univ.ContextSet.empty - end - in - let fn (name, b, t) = - let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in - if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - (* Declare the universe context once *) - let kind = Decls.(IsAssumption Logical) in - let decl = match b with - | None -> - Declare.ParameterEntry (None,(t,univs),None) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - Declare.DefinitionEntry entry - in - let cst = Declare.declare_constant ~name ~kind decl in - let env = Global.env () in - Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst); - () - else + let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in + let ctx = named_of_rel_context ctx in + (* reorder, evar-normalize and add implicit status *) + let ctx = List.rev_map (fun (name,b,t) -> + let b = Option.map (EConstr.to_constr sigma) b in + let t = EConstr.to_constr sigma t in let test x = match x.CAst.v with | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in - let scope = - if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in - match b with - | None -> - let _, _ = - declare_assumption false ~scope ~poly ~kind:Decls.Context t - univs UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make name) - in - () - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition - ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] in - () + let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in + name,b,t,impl) + ctx in - List.iter fn (List.rev ctx) + if Lib.sections_are_opened () + then context_insection sigma ~poly ctx + else context_nosection sigma ~poly ctx + +(* Deprecated *) +let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl name = +let open DeclareDef in +match scope with +| Discharge -> + let univs = match univs with + | Monomorphic_entry univs -> univs + | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs + in + let () = Declare.declare_universe_context ~poly univs in + declare_variable is_coe ~kind typ imps impl name; + GlobRef.VarRef name.CAst.v, Univ.Instance.empty +| Global local -> + declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl name diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 44db47e1cc..ae9edefcac 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -23,27 +23,46 @@ val do_assumptions -> (ident_decl list * constr_expr) with_coercion list -> unit -(** returns [false] if the assumption is neither local to a section, - nor in a module type and meant to be instantiated. *) -val declare_assumption +val declare_variable : coercion_flag - -> poly:bool - -> scope:DeclareDef.locality -> kind:Decls.assumption_object_kind -> Constr.types - -> Entries.universes_entry - -> UnivNames.universe_binders -> Impargs.manual_implicits -> Glob_term.binding_kind + -> variable CAst.t + -> unit + +val declare_axiom + : coercion_flag + -> poly:bool + -> local:Declare.import_status + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry * UnivNames.universe_binders + -> Impargs.manual_implicits -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t (** Context command *) -(** returns [false] if, for lack of section, it declares an assumption - (unless in a module type). *) val context : poly:bool -> local_binder_expr list -> unit + +(** Deprecated *) +val declare_assumption + : coercion_flag + -> poly:bool + -> scope:DeclareDef.locality + -> kind:Decls.assumption_object_kind + -> Constr.types + -> Entries.universes_entry + -> UnivNames.universe_binders + -> Impargs.manual_implicits + -> Glob_term.binding_kind + -> Declaremods.inline + -> variable CAst.t + -> GlobRef.t * Univ.Instance.t +[@@ocaml.deprecated "Use declare_variable or declare_axiom instead."] -- cgit v1.2.3 From d7f11221f797e501fe3bcdb06fe7ef3f559869c3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 19 Aug 2019 16:46:20 +0200 Subject: Fix #10669 incorrect substitution in context outside section --- vernac/comAssumption.ml | 76 ++++++++++++++++++++++++------------------------- 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'vernac') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 42c6250919..8cf5e3a8b4 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -53,6 +53,10 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in () +let instance_of_univ_entry = function + | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs + | Monomorphic_entry _ -> Univ.Instance.empty + let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} = let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with @@ -75,10 +79,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name | Declare.ImportDefaultBehavior -> false in let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in - let inst = match univs with - | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs - | Monomorphic_entry _ -> Univ.Instance.empty - in + let inst = instance_of_univ_entry univs in (gr,inst) let interp_assumption ~program_mode sigma env impls c = @@ -197,40 +198,33 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let ubinders = Evd.universe_binders sigma in declare_assumptions ~poly ~scope ~kind (univs,ubinders) nl l -let named_of_rel_context l = - let acc, ctx = - List.fold_right - (fun decl (subst, ctx) -> - let d = RelDecl.(to_tuple (map_constr (EConstr.Vars.substl subst) decl)) in - let id, _, _ as d = on_pi1 (fun annot -> - match binder_name annot with - | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") - | Name id -> id) - d - in - (EConstr.mkVar id :: subst, d :: ctx)) - l ([], []) - in ctx +let context_subst subst (name,b,t,impl) = + name, Option.map (Vars.substl subst) b, Vars.substl subst t, impl let context_insection sigma ~poly ctx = let uctx = Evd.universe_context_set sigma in let () = Declare.declare_universe_context ~poly uctx in - let fn = function - | name, None, t, impl -> - let kind = Decls.Context in - declare_variable false ~kind t [] impl (CAst.make name) - | name, Some b, t, impl -> - (* We need to get poly right for check_same_poly *) - let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) - else Monomorphic_entry Univ.ContextSet.empty - in - let entry = Declare.definition_entry ~univs ~types:t b in - let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] - in - () + let fn subst (name,_,_,_ as d) = + let d = context_subst subst d in + let () = match d with + | name, None, t, impl -> + let kind = Decls.Context in + declare_variable false ~kind t [] impl (CAst.make name) + | name, Some b, t, impl -> + (* We need to get poly right for check_same_poly *) + let univs = if poly then Polymorphic_entry ([| |], Univ.UContext.empty) + else Monomorphic_entry Univ.ContextSet.empty + in + let entry = Declare.definition_entry ~univs ~types:t b in + let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge + ~kind:Decls.Definition UnivNames.empty_binders entry [] + in + () + in + Constr.mkVar name :: subst in - List.iter fn ctx + let _ : Vars.substl = List.fold_left fn [] ctx in + () let context_nosection sigma ~poly ctx = let univs = @@ -243,7 +237,8 @@ let context_nosection sigma ~poly ctx = let () = Declare.declare_universe_context ~poly uctx in Monomorphic_entry Univ.ContextSet.empty in - let fn (name,b,t,_impl) = + let fn subst d = + let (name,b,t,_impl) = context_subst subst d in let kind = Decls.(IsAssumption Logical) in let decl = match b with | None -> @@ -260,9 +255,10 @@ let context_nosection sigma ~poly ctx = let () = if Lib.is_modtype() || Option.is_empty b then Classes.declare_instance env sigma None (Lib.is_modtype()) (GlobRef.ConstRef cst) in - () + Constr.mkConstU (cst,instance_of_univ_entry univs) :: subst in - List.iter fn ctx + let _ : Vars.substl = List.fold_left fn [] ctx in + () let context ~poly l = let env = Global.env() in @@ -272,9 +268,13 @@ let context ~poly l = let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in - let ctx = named_of_rel_context ctx in (* reorder, evar-normalize and add implicit status *) - let ctx = List.rev_map (fun (name,b,t) -> + let ctx = List.rev_map (fun d -> + let {binder_name=name}, b, t = RelDecl.to_tuple d in + let name = match name with + | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") + | Name id -> id + in let b = Option.map (EConstr.to_constr sigma) b in let t = EConstr.to_constr sigma t in let test x = match x.CAst.v with -- cgit v1.2.3