diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 19:08:22 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 20:36:36 -0400 |
| commit | c9f7a31ef67ce638ec591f9e5760941706bc12bc (patch) | |
| tree | 21963d1559d6dca5d173f270e4a6b22d76369be4 | |
| parent | d050094c578bdf5fc0611b808949fee28ae2a641 (diff) | |
[save proof] Declare universe_binders unconditionally for mutual assumptions.
As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
| -rw-r--r-- | vernac/declareDef.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index ba4b42c4e0..bd857a6e38 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -87,6 +87,8 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let kn = Declare.declare_constant ~name ~local ~kind decl in let dref = Names.GlobRef.ConstRef kn in let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = Declare.assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in dref diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1d3132d525..5eacd7aca7 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -255,9 +255,6 @@ let compute_proof_using_for_admitted proof typ pproofs = let finish_admitted ~name ~poly ~scope pe uctx hook ~udecl impargs other_thms = let dref = DeclareDef.declare_assumption ~name ~scope ~hook ~uctx ~impargs pe in - (* Should both of those be done in declare_axiom? *) - let () = Declare.assumption_message name in - DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx); process_recthms ?fix_exn:None ?hook uctx ~udecl ~poly ~scope dref other_thms let save_lemma_admitted ~(lemma : t) : unit = |