5 files changed, 69 insertions, 0 deletions

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 026f23749..b2df95901 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -24,6 +24,7 @@ val notation_constr_of_glob_constr :
 val ldots_var : identifier
 
 (** Equality of [glob_constr] (warning: only partially implemented) *)
+(** FIXME: nothing to do here *)
 val eq_glob_constr : glob_constr -> glob_constr -> bool
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 7ef0bd1f7..8bd8dc217 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -33,6 +33,13 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
+let glob_sort_eq g1 g2 = match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType None, GType None -> true
+| GType (Some s1), GType (Some s2) -> String.equal s1 s2
+| _ -> false
+
 let map_glob_constr_left_to_right f = function
   | GApp (loc,g,args) ->
       let comp1 = f g in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 0941b0c8b..ed2d0ae2d 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -17,6 +17,9 @@ open Misctypes
 open Locus
 open Glob_term
 
+(** Equalities *)
+val glob_sort_eq : glob_sort -> glob_sort -> bool
+
 (** Operations on [glob_constr] *)
 
 val cases_pattern_loc : cases_pattern -> Loc.t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index bd08df533..0c21cb805 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -21,6 +21,62 @@ open Decl_kinds
 open Pattern
 open Evd
 
+let case_info_pattern_eq i1 i2 =
+  i1.cip_style == i2.cip_style &&
+  Option.Misc.compare eq_ind i1.cip_ind i2.cip_ind &&
+  Option.Misc.compare Int.equal i1.cip_ind_args i2.cip_ind_args &&
+  i1.cip_extensible == i2.cip_extensible
+
+let rec constr_pattern_eq p1 p2 = match p1, p2 with
+| PRef r1, PRef r2 -> eq_gr r1 r2
+| PVar v1, PVar v2 -> id_eq v1 v2
+| PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
+  Int.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
+| PRel i1, PRel i2 ->
+  Int.equal i1 i2
+| PApp (t1, arg1), PApp (t2, arg2) ->
+  constr_pattern_eq t1 t2 && Array.equal constr_pattern_eq arg1 arg2
+| PSoApp (id1, arg1), PSoApp (id2, arg2) ->
+  id_eq id1 id2 && List.equal constr_pattern_eq arg1 arg2
+| PLambda (v1, t1, b1), PLambda (v2, t2, b2) ->
+  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+| PProd (v1, t1, b1), PProd (v2, t2, b2) ->
+  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
+  name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+| PSort s1, PSort s2 -> glob_sort_eq s1 s2
+| PMeta m1, PMeta m2 -> Option.Misc.compare id_eq m1 m2
+| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
+  constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
+| PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
+  case_info_pattern_eq info1 info2 &&
+  constr_pattern_eq p1 p2 &&
+  constr_pattern_eq r1 r2 &&
+  List.equal pattern_eq l1 l2
+| PFix f1, PFix f2 ->
+  fixpoint_eq f1 f2
+| PCoFix f1, PCoFix f2 ->
+  cofixpoint_eq f1 f2
+| _ -> false
+(** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
+
+and pattern_eq (i1, j1, p1) (i2, j2, p2) =
+  Int.equal i1 i2 && Int.equal j1 j2 && constr_pattern_eq p1 p2
+
+and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
+  Int.equal i1 i2 &&
+  Array.equal Int.equal arg1 arg2 &&
+  rec_declaration_eq r1 r2
+
+and cofixpoint_eq (i1, r1) (i2, r2) =
+  Int.equal i1 i2 &&
+  rec_declaration_eq r1 r2
+
+and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
+  Array.equal name_eq n1 n2 &&
+  Array.equal eq_constr c1 c2 &&
+  Array.equal eq_constr r1 r2
+
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
       (occur_meta_pattern f) or (Array.exists occur_meta_pattern args)
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 835733733..b20510b86 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -20,6 +20,8 @@ open Pattern
 
 (** {5 Functions on patterns} *)
 
+val constr_pattern_eq : constr_pattern -> constr_pattern -> bool
+
 val occur_meta_pattern : constr_pattern -> bool
 
 val subst_pattern : substitution -> constr_pattern -> constr_pattern