diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /interp | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 7 | ||||
| -rw-r--r-- | interp/notation.ml | 1 |
2 files changed, 0 insertions, 8 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index b8f97e77c..011b31d9a 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -8,7 +8,6 @@ open Loc open Tacexpr -open Term open Misctypes open Genarg open Geninterp @@ -49,9 +48,6 @@ let wit_quant_hyp = make0 "quant_hyp" let wit_constr = make0 "constr" -let wit_constr_may_eval = - make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" - let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" @@ -60,9 +56,6 @@ let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_bindings = make0 "bindings" -let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = - make0 "hyp_location_flag" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = diff --git a/interp/notation.ml b/interp/notation.ml index b8f4f3201..0a65dfc09 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -13,7 +13,6 @@ open Pp open Bigint open Names open Term -open Nametab open Libnames open Globnames open Constrexpr |