Ccproof: generic equality on term replaced by term_equal

... and define term_equal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14342 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 14 insertions, 1 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 18dbecb667..b7acaf5b67 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -103,6 +103,17 @@ type term=
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
+let rec term_equal t1 t2 =
+  match t1, t2 with
+    | Symb c1, Symb c2 -> eq_constr c1 c2
+    | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
+    | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+    | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
+    | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
+      Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
+      i1 = i2 && j1 = j2 && eq_constructor c1 c2
+    | _ -> t1 = t2
+
 type ccpattern =
     PApp of term * ccpattern list (* arguments are reversed *)
   | PVar of int
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 9466b611e1..326fffb790 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -22,6 +22,8 @@ type term =
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
+val term_equal : term -> term -> bool
+
 type patt_kind =
     Normal
   | Trivial of types
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 313d192052..36bdd0b17b 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -43,7 +43,7 @@ let rec ptrans p1 p3=
     | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
 	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
   | _, _ ->
-      if p1.p_rhs = p3.p_lhs then
+      if term_equal p1.p_rhs p3.p_lhs then
 	{p_lhs=p1.p_lhs;
 	 p_rhs=p3.p_rhs;
 	 p_rule=Trans (p1,p3)}