3 files changed, 114 insertions, 2 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index bd61ba28f..5066e2e22 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -526,7 +526,7 @@ let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
     | _, GHole _ ->
       add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v
     | _, _ ->
-        if Pervasives.(=) v v' then fullsigma (** FIXME *)
+        if glob_constr_eq v v' then fullsigma
         else raise No_match
   with Not_found -> add_env alp fullsigma var v
 
@@ -791,7 +791,7 @@ let add_patterns_for_params ind l =
 let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
     let vvar = Id.List.assoc var sigma in
-    if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *)
+    if cases_pattern_eq v vvar then fullsigma else raise No_match
   with Not_found ->
     (* TODO: handle the case of multiple occs in different scopes *)
     (var,v)::sigma,sigmalist,x
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index b847a1390..9fc981a7d 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -33,6 +33,19 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
+let binding_kind_eq bk1 bk2 = match bk1, bk2 with
+| Decl_kinds.Explicit, Decl_kinds.Explicit -> true
+| Decl_kinds.Implicit, Decl_kinds.Implicit -> true
+| _ -> false
+
+let case_style_eq s1 s2 = match s1, s2 with
+| LetStyle, LetStyle -> true
+| IfStyle, IfStyle -> true
+| LetPatternStyle, LetPatternStyle -> true
+| MatchStyle, MatchStyle -> true
+| RegularStyle, RegularStyle -> true
+| _ -> false
+
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
@@ -40,6 +53,101 @@ let glob_sort_eq g1 g2 = match g1, g2 with
 | GType (Some s1), GType (Some s2) -> String.equal s1 s2
 | _ -> false
 
+let rec cases_pattern_eq p1 p2 = match p1, p2 with
+| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
+| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
+  eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+  Name.equal na1 na2
+| _ -> false
+
+let cast_type_eq eq t1 t2 = match t1, t2 with
+| CastConv t1, CastConv t2 -> eq t1 t2
+| CastVM t1, CastVM t2 -> eq t1 t2
+| CastCoerce, CastCoerce -> true
+| CastNative t1, CastNative t2 -> eq t1 t2
+| _ -> false
+
+let eq_gr gr1 gr2 = match gr1, gr2 with
+| ConstRef con1, ConstRef con2 -> eq_constant con1 con2
+| IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
+| ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
+| VarRef v1, VarRef v2 -> Id.equal v1 v2
+| _ -> false
+
+let rec glob_constr_eq c1 c2 = match c1, c2 with
+| GRef (_, gr1), GRef (_, gr2) -> eq_gr gr1 gr2
+| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
+| GEvar (_, ev1, arg1), GEvar (_, ev2, arg2) ->
+  Evar.equal ev1 ev2 &&
+  Option.equal (fun l1 l2 -> List.equal glob_constr_eq l1 l2) arg1 arg2
+| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+  (b1 : bool) == b2 && Id.equal pat1 pat2
+| GApp (_, f1, arg1), GApp (_, f2, arg2) ->
+  glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
+| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) ->
+  Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
+  glob_constr_eq t1 t2 && glob_constr_eq c1 c2
+| GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) ->
+  Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
+  glob_constr_eq t1 t2 && glob_constr_eq c1 c2
+| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) ->
+  Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2
+| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) ->
+  case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
+  List.equal tomatch_tuple_eq tp1 tp2 &&
+  List.equal cases_clause_eq cl1 cl2
+| GLetTuple (_, na1, (n1, p1), c1, t1), GLetTuple (_, na2, (n2, p2), c2, t2) ->
+  List.equal Name.equal na1 na2 && Name.equal n1 n2 &&
+  Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
+  glob_constr_eq t1 t2
+| GIf (_, m1, (pat1, p1), c1, t1), GIf (_, m2, (pat2, p2), c2, t2) ->
+  glob_constr_eq m1 m2 && Name.equal pat1 pat2 &&
+  Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
+  glob_constr_eq t1 t2
+| GRec (_, kn1, id1, decl1, c1, t1), GRec (_, kn2, id2, decl2, c2, t2) ->
+  fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
+  Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
+  Array.equal glob_constr_eq c1 c2 &&
+  Array.equal glob_constr_eq t1 t2
+| GSort (_, s1), GSort (_, s2) -> glob_sort_eq s1 s2
+| GHole (_, kn1, gn1), GHole (_, kn2, gn2) ->
+  Option.equal (==) gn1 gn2 (** Only thing sensible *)
+| GCast (_, c1, t1), GCast (_, c2, t2) ->
+  glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2
+| _ -> false
+
+and tomatch_tuple_eq (c1, p1) (c2, p2) =
+  let eqp (_, i1, na1) (_, i2, na2) =
+    eq_ind i1 i2 && List.equal Name.equal na1 na2
+  in
+  let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
+  glob_constr_eq c1 c2 && eq_pred p1 p2
+
+and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) =
+  List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 &&
+  glob_constr_eq c1 c2
+
+and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
+  Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
+  Option.equal glob_constr_eq c1 c2 &&
+  glob_constr_eq t1 t2
+
+and fix_kind_eq k1 k2 = match k1, k2 with
+| GFix (a1, i1), GFix (a2, i2) ->
+  let eq (i1, o1) (i2, o2) =
+    Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2
+  in
+  Int.equal i1 i2 && Array.equal eq a1 a1
+| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
+| _ -> false
+
+and fix_recursion_order_eq o1 o2 = match o1, o2 with
+| GStructRec, GStructRec -> true
+| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2
+| GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
+  glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2
+| _ -> 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 4e8224879..5195b98c8 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -20,6 +20,10 @@ open Glob_term
 (** Equalities *)
 val glob_sort_eq : glob_sort -> glob_sort -> bool
 
+val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
+
+val glob_constr_eq : glob_constr -> glob_constr -> bool
+
 (** Operations on [glob_constr] *)
 
 val cases_pattern_loc : cases_pattern -> Loc.t