From 00d0ae561f738b19cfef14ce94cc056206e9c1bc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 Apr 2002 20:41:07 +0000
Subject: Suppression de l'application de f_equal2 pour "mult" (non
 inversible); Application de f_equal2 pour "plus" seulement si soit les
 membres droits soit les membres gauches sont égaux.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2616 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/ring.ml | 29 ++++++++++++++++++-----------
 1 file changed, 18 insertions(+), 11 deletions(-)

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index dabf68892a..e6635c441b 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -887,18 +887,26 @@ let raw_polynom th op lc gl =
   in
   polynom_tac gl
 
-let guess_eq_tac th = 
+let guess_eq_tac th =
   (tclORELSE reflexivity
-     (tclTHEN 
+     (tclTHEN
 	polynom_unfold_tac
-	(tclREPEAT 
-	   (tclORELSE 
-	      (apply (mkApp(build_coq_f_equal2 (),
-		            [| th.th_a; th.th_a; th.th_a;
-			       th.th_plus |])))
-	      (apply (mkApp(build_coq_f_equal2 (),
-		            [| th.th_a; th.th_a; th.th_a; 
-			       th.th_mult |])))))))
+        (tclTHEN
+	   (* Normalized sums associate on the right *)
+	   (tclREPEAT
+	      (tclTHENST
+		 (apply (mkApp(build_coq_f_equal2 (),
+		               [| th.th_a; th.th_a; th.th_a;
+				  th.th_plus |])))
+		 [reflexivity]
+		 tclIDTAC))
+	   (tclTRY
+	      (tclTHENL
+		 (apply (mkApp(build_coq_f_equal2 (),
+			       [| th.th_a; th.th_a; th.th_a;
+				  th.th_plus |])))
+		 reflexivity)))))
+
 let guess_equiv_tac th = 
   (tclORELSE (apply (mkLApp(coq_seq_refl,
 			    [| th.th_a; (unbox th.th_equiv);
@@ -966,4 +974,3 @@ let dyn_polynom ltacargs gl =
 	     ltacargs) gl
 
 let v_polynom = add_tactic "Ring" dyn_polynom
-
-- 
cgit v1.2.3