diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-03 20:49:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:47:12 +0200 |
| commit | c7fd62135403c1ea38194fcdd8035237ee108318 (patch) | |
| tree | 4fc94b097de3969dfe71121865c8e19b276cb38c /interp | |
| parent | 729d838838d8df06395726477817620e2ae998bc (diff) | |
Removing useless generic arguments.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 3 | ||||
| -rw-r--r-- | interp/constrarg.mli | 9 |
2 files changed, 0 insertions, 12 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 99f0a2da6..b8f97e77c 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -46,9 +46,6 @@ let wit_ref = make0 "ref" let wit_quant_hyp = make0 "quant_hyp" -let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - make0 "sort" - let wit_constr = make0 "constr" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 6407b61af..70c9c0de2 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -38,15 +38,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_sort : (glob_sort, glob_sort, sorts) genarg_type - val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_may_eval : - ((constr_expr,reference or_by_notation,constr_expr) may_eval, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, - constr) genarg_type - val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : @@ -62,8 +55,6 @@ val wit_bindings : glob_constr_and_expr bindings, constr bindings delayed_open) genarg_type -val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type - val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, |