diff options
| author | ppedrot | 2012-11-25 17:38:55 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-25 17:38:55 +0000 |
| commit | 1653654a0eba7ecca78e67b4db1f6fa031e7271f (patch) | |
| tree | e5a914ecf08ebddc774216122d3910fb8ecee9b9 /interp/genarg.ml | |
| parent | 589b1edc7064c2d210cf4786a6e5ed32d8165117 (diff) | |
More equality functions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/genarg.ml')
| -rw-r--r-- | interp/genarg.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 9e3528cf41..1192423c2c 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -36,6 +36,32 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string +let rec argument_type_eq arg1 arg2 = match arg1, arg2 with +| BoolArgType, BoolArgType -> true +| IntArgType, IntArgType -> true +| IntOrVarArgType, IntOrVarArgType -> true +| StringArgType, StringArgType -> true +| PreIdentArgType, PreIdentArgType -> true +| IntroPatternArgType, IntroPatternArgType -> true +| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2 +| VarArgType, VarArgType -> true +| RefArgType, RefArgType -> true +| SortArgType, SortArgType -> true +| ConstrArgType, ConstrArgType -> true +| ConstrMayEvalArgType, ConstrMayEvalArgType -> true +| QuantHypArgType, QuantHypArgType -> true +| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2 +| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true +| BindingsArgType, BindingsArgType -> true +| RedExprArgType, RedExprArgType -> true +| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2 +| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2 +| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 +| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> + argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r +| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 +| _ -> false + let loc_of_or_by_notation f = function | AN c -> f c | ByNotation (loc,s,_) -> loc |