diff options
| author | bertot | 2006-10-05 13:17:26 +0000 |
|---|---|---|
| committer | bertot | 2006-10-05 13:17:26 +0000 |
| commit | 7cef572b8a4bbe8b5e0ceb5dce9bc07f09880885 (patch) | |
| tree | a5a723c5aedb3e4d13518ea4479208095b08208a | |
| parent | 19a8469f7accf0671bc0270c66d7725ae57f6720 (diff) | |
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
| -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. |