aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
authorppedrot2012-11-25 17:38:55 +0000
committerppedrot2012-11-25 17:38:55 +0000
commit1653654a0eba7ecca78e67b4db1f6fa031e7271f (patch)
treee5a914ecf08ebddc774216122d3910fb8ecee9b9 /interp/constrexpr_ops.ml
parent589b1edc7064c2d210cf4786a6e5ed32d8165117 (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/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 6b45c88975..b9469bdf37 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,6 +17,18 @@ open Decl_kinds
(***********************)
(* For binders parsing *)
+let binding_kind_eq bk1 bk2 = match bk1, bk2 with
+| Explicit, Explicit -> true
+| Implicit, Implicit -> true
+| _ -> false
+
+let binder_kind_eq b1 b2 = match b1, b2 with
+| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
+ binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+ (if b1 then b2 else not b2)
+| _ -> false
+
let default_binder_kind = Default Explicit
let names_of_local_assums bl =