diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 8 | ||||
| -rw-r--r-- | tactics/declare.mli | 4 |
2 files changed, 4 insertions, 8 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 91c55cacb0..c0eae7503c 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -308,19 +308,17 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind kn, eff (** Declaration of section variables and local definitions *) -type section_variable_entry = +type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } -type variable_declaration = DirPath.t * section_variable_entry - (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) let inVariable : unit -> obj = declare_object { (default_object "VARIABLE") with classify_function = (fun () -> Dispose)} -let declare_variable ~name ~kind (path,d) = +let declare_variable ~name ~kind d = (* Constr raisonne sur les noms courts *) if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); @@ -359,7 +357,7 @@ let declare_variable ~name ~kind (path,d) = in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); add_section_variable ~name ~kind:impl ~poly univs; - Decls.(add_variable_data name {path;opaque;kind}); + Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) diff --git a/tactics/declare.mli b/tactics/declare.mli index 3edb3f29cd..89b41076f7 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -21,7 +21,7 @@ open Entries (** Declaration of local constructions (Variable/Hypothesis/Local) *) -type section_variable_entry = +type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } @@ -30,8 +30,6 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -type variable_declaration = DirPath.t * section_variable_entry - val declare_variable : name:variable -> kind:Decls.logical_kind |