From 7cef572b8a4bbe8b5e0ceb5dce9bc07f09880885 Mon Sep 17 00:00:00 2001
From: bertot
Date: Thu, 5 Oct 2006 13:17:26 +0000
Subject: A version of natprering that should be more efficient and removal of
 a bad comment in newring.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9212 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/setoid_ring/ArithRing.v | 13 +++++++++++--
 contrib/setoid_ring/newring.ml4 | 20 --------------------
 theories/ZArith/Zcomplements.v  |  2 +-
 3 files changed, 12 insertions(+), 23 deletions(-)

diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 70554372ab..0f99432dc0 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -23,13 +23,22 @@ Ltac natcst t :=
   | _ => NotConstant
   end.
 
+Ltac Ss_to_add f acc :=
+  match f with
+  | S ?f1 => Ss_to_add f1 (S acc)
+  | _ => constr:(acc + f)%nat
+  end.
+
 Ltac natprering :=
   match goal with
     |- context C [S ?p] =>
     match p with
       O => fail 1 (* avoid replacing 1 with 1+0 ! *)
-    | S _ => fail 1
-    | _ => fold (1+p)%nat; natprering
+    | p => match isnatcst p with 
+           | true => fail 1
+           | false => let v := Ss_to_add p (S 0) in
+                         fold v; natprering
+           end
     end
   | _ => idtac
   end.
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 97d6c32914..0468438668 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -717,26 +717,6 @@ let ring_rewrite rl gl =
 			       List.map carg 
 			       [e.ring_lemma2; e.ring_req; rl])))) gl)
 	(Tacinterp.eval_tactic e.ring_post_tac)) gl
-(*
-  Tacinterp.eval_tactic
-    (TacThen
-	(e.ring_pre_tac,
-	TacThen
-	  (TacArg(TacCall(dummy_loc,
-            (ArgArg(dumm_loc, 
-	      fun gl ->
-		let rl = 
-		  match rl with
-		      [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2]
-		    | _ -> rl in
-		let rl = List.fold_right
-		  (fun x l -> lapp coq_cons [|e.ring_carrier;x;l|]) rl
-		  (lapp coq_nil [|e.ring_carrier|]) in
-	      Lazy.force ltac_setoid_ring_rewrite
-		(Tacexp e.ring_cst_tac::
-		    List.map carg [e.ring_lemma2; e.ring_req; rl]) gl)))),
-	    e.ring_post_tac))) gl
-*)
 
 TACTIC EXTEND setoid_ring
   [ "ring" ] -> [ ring ]
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index a3f17f4d8f..e5c18bd33d 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import ZArithRing.
+Require Export ZArithRing.
 Require Import ZArith_base.
 Require Import Omega.
 Require Import Wf_nat.
-- 
cgit v1.2.3