diff options
| -rw-r--r-- | contrib/setoid_ring/ArithRing.v | 13 | ||||
| -rw-r--r-- | contrib/setoid_ring/newring.ml4 | 20 | ||||
| -rw-r--r-- | 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. |