diff options
| author | xclerc | 2013-12-02 13:09:42 +0100 |
|---|---|---|
| committer | xclerc | 2013-12-02 13:09:42 +0100 |
| commit | 76d4622212e7c5596eb03fd17ff0177b6c44a990 (patch) | |
| tree | 480237faebb6b2dae88f0c157c4307109105aec7 /lib | |
| parent | c101a710c96e03e228e4b1aacee8edebd3c8dabf (diff) | |
| parent | cb290d81c46ec370e303e1414e203c40c8fa1174 (diff) | |
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into trunk
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/genarg.ml | 9 | ||||
| -rw-r--r-- | lib/genarg.mli | 3 |
2 files changed, 4 insertions, 8 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml index 98287d1842..6520669fa6 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -14,13 +14,12 @@ type argument_type = | IntOrVarArgType | IdentArgType of bool | VarArgType - | RefArgType (* Specific types *) | GenArgType | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType @@ -33,12 +32,11 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | IntOrVarArgType, IntOrVarArgType -> true | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 | VarArgType, VarArgType -> true -| RefArgType, RefArgType -> true | GenArgType, GenArgType -> true | ConstrArgType, ConstrArgType -> true | ConstrMayEvalArgType, ConstrMayEvalArgType -> true | QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 +| OpenConstrArgType, OpenConstrArgType -> true | ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true | BindingsArgType, BindingsArgType -> true | RedExprArgType, RedExprArgType -> true @@ -54,12 +52,11 @@ let rec pr_argument_type = function | IdentArgType true -> str "ident" | IdentArgType false -> str "pattern_ident" | VarArgType -> str "var" -| RefArgType -> str "ref" | GenArgType -> str "genarg" | ConstrArgType -> str "constr" | ConstrMayEvalArgType -> str "constr_may_eval" | QuantHypArgType -> str "qhyp" -| OpenConstrArgType _ -> str "open_constr" +| OpenConstrArgType -> str "open_constr" | ConstrWithBindingsArgType -> str "constr_with_bindings" | BindingsArgType -> str "bindings" | RedExprArgType -> str "redexp" diff --git a/lib/genarg.mli b/lib/genarg.mli index e2654fcf57..51c261742e 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -193,13 +193,12 @@ type argument_type = | IntOrVarArgType | IdentArgType of bool | VarArgType - | RefArgType (** Specific types *) | GenArgType | ConstrArgType | ConstrMayEvalArgType | QuantHypArgType - | OpenConstrArgType of bool + | OpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType |