diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-16 20:03:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-17 13:44:00 +0100 |
| commit | 597e5dd737dd235222798153b2342ae609519348 (patch) | |
| tree | 283c27ba7ce6be305affbc54a9e1c8813c3ece30 /lib/genarg.ml | |
| parent | 7fa49442f30dceb7e403fb5dab660002dda7f6e9 (diff) | |
Getting rid of some hardwired generic arguments.
Diffstat (limited to 'lib/genarg.ml')
| -rw-r--r-- | lib/genarg.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 149d872c5..8712eda8e 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -18,11 +18,7 @@ type argument_type = | GenArgType | ConstrArgType | ConstrMayEvalArgType - | QuantHypArgType | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type @@ -35,11 +31,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | GenArgType, GenArgType -> true | ConstrArgType, ConstrArgType -> true | ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true | OpenConstrArgType, OpenConstrArgType -> true -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 | PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> @@ -54,11 +46,7 @@ let rec pr_argument_type = function | GenArgType -> str "genarg" | ConstrArgType -> str "constr" | ConstrMayEvalArgType -> str "constr_may_eval" -| QuantHypArgType -> str "qhyp" | OpenConstrArgType -> str "open_constr" -| ConstrWithBindingsArgType -> str "constr_with_bindings" -| BindingsArgType -> str "bindings" -| RedExprArgType -> str "redexp" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> |