diff options
| author | Gaëtan Gilbert | 2019-07-02 13:59:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | bffe3e43a51420293960cc3c32845687bdee5f9b (patch) | |
| tree | 8928e9137f1652552d5c394c6d040aeb888812c5 | |
| parent | 48a377680f4f3b96f7c19c22f5641877c561f03d (diff) | |
Remove unused Decls.variable_{context,polymorphic}
| -rw-r--r-- | interp/decls.ml | 4 | ||||
| -rw-r--r-- | interp/decls.mli | 4 | ||||
| -rw-r--r-- | tactics/declare.ml | 2 |
3 files changed, 1 insertions, 9 deletions
diff --git a/interp/decls.ml b/interp/decls.ml index b802dbe9c3..ec5d4fa3cb 100644 --- a/interp/decls.ml +++ b/interp/decls.ml @@ -62,8 +62,6 @@ type logical_kind = type variable_data = { path:DirPath.t ; opaque:bool - ; univs:Univ.ContextSet.t - ; poly:bool ; kind:logical_kind } @@ -75,8 +73,6 @@ let add_variable_data id o = vartab := Id.Map.add id o !vartab let variable_path id = let {path} = Id.Map.find id !vartab in path let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque let variable_kind id = let {kind} = Id.Map.find id !vartab in kind -let variable_context id = let {univs} = Id.Map.find id !vartab in univs -let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in diff --git a/interp/decls.mli b/interp/decls.mli index 05e4be0de6..2a11a271cc 100644 --- a/interp/decls.mli +++ b/interp/decls.mli @@ -63,8 +63,6 @@ type logical_kind = type variable_data = { path:DirPath.t ; opaque:bool - ; univs:Univ.ContextSet.t - ; poly:bool ; kind:logical_kind } @@ -81,6 +79,4 @@ val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool (* Used in declare, very dubious *) -val variable_context : variable -> Univ.ContextSet.t -val variable_polymorphic : variable -> bool val variable_exists : variable -> bool diff --git a/tactics/declare.ml b/tactics/declare.ml index da3a119a79..91c55cacb0 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -359,7 +359,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;univs;poly;kind}); + Decls.(add_variable_data name {path;opaque;kind}); add_anonymous_leaf (inVariable ()); Impargs.declare_var_implicits name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) |