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 /tactics | |
| parent | 48a377680f4f3b96f7c19c22f5641877c561f03d (diff) | |
Remove unused Decls.variable_{context,polymorphic}
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |