diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:11:47 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
| commit | 4e84e83911c1cf7613a35b921b1e68e097f84b5a (patch) | |
| tree | 86caa28a08dde1e771c365350550ffdd633ba1f8 /interp | |
| parent | e1d2a898feacbe4bd363818f259bce5fd74c2ee7 (diff) | |
Remove unused [open] statements
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.mli | 1 | ||||
| -rw-r--r-- | interp/stdarg.ml | 2 | ||||
| -rw-r--r-- | interp/stdarg.mli | 1 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
5 files changed, 0 insertions, 8 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf..389880c5c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t = let t' = locate_if_hole (loc_of_glob_constr t) na t in understand_tcc_evars env evdref ~expected_type:IsType t' -open Environ - let my_intern_constr env lvar acc c = internalize env acc false lvar c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 758d4e650..fdd50c6a1 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,7 +18,6 @@ open Constrexpr open Notation_term open Pretyping open Misctypes -open Decl_kinds (** Translation from front abstract syntax of term to untyped terms (glob_constr) *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 341ff5662..5920b0d50 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Misctypes -open Tactypes open Genarg open Geninterp diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 113fe40ba..ac40a2328 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -10,7 +10,6 @@ open Loc open Names -open Term open EConstr open Libnames open Globnames diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index c3f4c4f30..ed7b0b70d 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -106,5 +106,3 @@ let search_syntactic_definition kn = let def = out_pat pat in verbose_compat kn def v; def - -open Goptions |