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/constrarg.ml | |
| parent | 729d838838d8df06395726477817620e2ae998bc (diff) | |
Removing useless generic arguments.
Diffstat (limited to 'interp/constrarg.ml')
| -rw-r--r-- | interp/constrarg.ml | 3 |
1 files changed, 0 insertions, 3 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" |