diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 04:57:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 (patch) | |
| tree | cd73ab17e32bbe46c422208469c912f87968fc47 /interp/stdarg.ml | |
| parent | 368a25e4ef14512b00f5799e26c3f615bc540201 (diff) | |
[api] Misctypes removal: move Tactypes to proofs
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
Diffstat (limited to 'interp/stdarg.ml')
| -rw-r--r-- | interp/stdarg.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e5ed58be6..7a7bb9a84 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -34,9 +34,6 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" -let wit_intro_pattern = - make0 "intropattern" - let wit_ident = make0 "ident" @@ -45,8 +42,6 @@ let wit_var = let wit_ref = make0 "ref" -let wit_quant_hyp = make0 "quant_hyp" - let wit_sort_family = make0 "sort_family" let wit_constr = @@ -56,12 +51,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" - -let wit_bindings = make0 "bindings" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = @@ -74,6 +63,4 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern let wit_redexpr = wit_red_expr |