diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-23 11:09:12 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-23 11:09:12 +0000 |
commit | 73cc39bcd5edfd5feee97033b92e6be8af7f64c8 (patch) | |
tree | c27e2b4257d5539536dfede6f69305f4ae7e7e29 | |
parent | 90a2cea28df5ecdf9e2cdc4351aad5f6a993a003 (diff) |
ring : Correction du bug PR#1306
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9520 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 22 |
1 files changed, 17 insertions, 5 deletions
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 !!!!!!!!!!!!! *) |