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

2 files changed, 11 insertions, 22 deletions

diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 70554372a..0f99432dc 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 97d6c3291..046843866 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 ]