diff options
| author | Gaëtan Gilbert | 2019-08-18 19:46:50 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-05 12:10:24 +0200 |
| commit | 9f6e238fac96a123e7cb2bb2b2caec104bc4b916 (patch) | |
| tree | 08c10e60d141988ed5a393bd3b67934607f6326b /tactics | |
| parent | d5f2e13e51c3404d326f04513a50d264790a7a4c (diff) | |
Declare universes for variables outside of Declare.declare_variable
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
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 |