diff options
| author | Pierre-Marie Pédrot | 2015-12-18 17:18:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | 329b5b9ed526d572d7df066dc99486e1dcb9e4cc (patch) | |
| tree | 1cad1cd1c7371c8cefc9287dd32d190e12757d1c /lib/genarg.mli | |
| parent | b2beb9087628de23679a831e6273b91816f1ed27 (diff) | |
Removing the now useless genarg generic argument.
Diffstat (limited to 'lib/genarg.mli')
| -rw-r--r-- | lib/genarg.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli index c431aa619d..89ea49ddb5 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -205,7 +205,6 @@ type argument_type = | IdentArgType | VarArgType (** Specific types *) - | GenArgType | ConstrArgType | ConstrMayEvalArgType | OpenConstrArgType |