From 73cc39bcd5edfd5feee97033b92e6be8af7f64c8 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Tue, 23 Jan 2007 11:09:12 +0000 Subject: ring : Correction du bug PR#1306 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9520 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/setoid_ring/Ring_tac.v | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) (limited to 'contrib') diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index fbaff6e88..b6cfd914d 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -239,23 +239,35 @@ Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := (* Simplification *) - Ltac Ring_simplify_gen f := fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + let l := fresh "to_rewrite" in + pose (l:= rl); + generalize (refl_equal l); + unfold l at 2; pre(); - Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH rl; - post(). + match goal with + | [|- l = ?RL -> _ ] => + let Heq := fresh "Heq" in + intros Heq;clear Heq l; + Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; + post() + | _ => fail 1 "ring_simplify anomaly: bad goal after pre" + end. Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). Tactic Notation (at level 0) - "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := + "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end. Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end. + let Main := + match goal with [|- ?G] => (fun f => f G) end in + let Aux G := ring_lookup Ring_simplify [] rl [G] in + Main Aux. (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) -- cgit v1.2.3