diff options
| author | Pierre-Marie Pédrot | 2018-11-13 19:44:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-13 19:44:07 +0100 |
| commit | d384f58e5d910ec14574488f2744011cb09aa932 (patch) | |
| tree | 2b14c9d8bf601481ed96b84db31beb4689ce40ff /vernac | |
| parent | 3e38d26233229d313d7a4c6015c7c15206c07305 (diff) | |
| parent | ccf995fd843f14ae8dfaf18177be6c2494faea35 (diff) | |
Merge PR #8760: Automatically generate names for universes.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comInductive.ml | 2 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 5 |
3 files changed, 8 insertions, 5 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 0c39458a57..f405c4d5a9 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -535,11 +535,11 @@ let declare_mutual_inductive_with_eliminations mie pl impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in + Declare.declare_univ_binders (IndRef (mind,0)) pl; List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; - Declare.declare_univ_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 35fb18e292..2fe03a8ec5 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook = | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - ConstRef kn in + let gr = ConstRef kn in + let () = Declare.declare_univ_binders gr pl in + gr + in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in Lemmas.call_hook fix_exn hook local gr; gr diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 150f2c6ee9..3b041b7065 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - ConstRef kn + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders uctx); + gr in definition_message id; - Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in |