diff options
| -rw-r--r-- | tactics/declare.ml | 12 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 3 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 3 |
4 files changed, 10 insertions, 10 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index e418240d3a..3ec6f884be 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -302,7 +302,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } + | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -315,11 +315,10 @@ let declare_variable ~name ~kind d = if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); - let impl,opaque,poly = match d with (* Fails if not well-typed *) - | SectionLocalAssum {typ;univs;poly;impl} -> - let () = declare_universe_context ~poly univs in + let impl,opaque = match d with (* Fails if not well-typed *) + | SectionLocalAssum {typ;impl} -> let () = Global.push_named_assum (name,typ) in - impl, true, poly + impl, true | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) @@ -342,8 +341,7 @@ let declare_variable ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Glob_term.Explicit, de.proof_entry_opaque, - poly + Glob_term.Explicit, de.proof_entry_opaque in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind}); diff --git a/tactics/declare.mli b/tactics/declare.mli index 4cb876cecb..d479b75a28 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -36,7 +36,7 @@ type 'a proof_entry = { type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } + | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } type 'a constant_entry = | DefinitionEntry of 'a proof_entry 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 -> |