diff options
| -rw-r--r-- | tactics/declare.ml | 4 | ||||
| -rw-r--r-- | tactics/declare.mli | 6 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index a149850a64..324007930a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -188,8 +188,8 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univc=Univ.ContextSet.empty) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,univc), eff); + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); proof_entry_secctx = section_vars; proof_entry_type = types; proof_entry_universes = univs; diff --git a/tactics/declare.mli b/tactics/declare.mli index 6ea08d5b0e..615cffeae7 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -64,9 +64,9 @@ val definition_entry -> ?types:types -> ?univs:Entries.universes_entry -> ?eff:Evd.side_effects - -> ?univc:Univ.ContextSet.t - (** Universe-constraints attached to the body-only, used in vio / - vio-delayed opaque constants *) + -> ?univsbody:Univ.ContextSet.t + (** Universe-constraints attached to the body-only, used in + vio-delayed opaque constants and private poly universes *) -> constr -> Evd.side_effects proof_entry diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index d7f4cb3b9a..d7dcc13e79 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -221,7 +221,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let utyp = UState.check_univ_decl ~poly ctx udecl in utyp, Univ.ContextSet.empty in - Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univc:ubody ~types:typ ~eff body + Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in { name; entries; uctx } |