diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 12 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 |
2 files changed, 6 insertions, 8 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 |