diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 22:19:36 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-17 22:19:36 +0000 |
| commit | 33d54f6692446e6006f9b89d0dfd64408a4051fe (patch) | |
| tree | 4731ac413f0b2322a4b94879199943916255d2f1 /plugins/setoid_ring/Ncring_polynom.v | |
| parent | e0dfeeba32d84d57157da699e9e622992e7ed258 (diff) | |
Fixing bug #2640 and variants of it (inconsistency between when and
how the names of an ltac expression are globalized - allowing the
expression to be a constr and in some initial context - and when and
how this ltac expression is interpreted - now expecting a pure tactic
in a different context).
This incidentally found a Ltac bug in Ncring_polynom!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Ncring_polynom.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index a3e14b30f..c0d315871 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -23,7 +23,7 @@ Context (C R:Type) `{Rh:Ring_morphism C R}. Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. - Ltac rsimpl := repeat (gen_rewrite || phiCR_comm). + Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm). Ltac add_push := gen_add_push . (* Definition of non commutative multivariable polynomials @@ -298,7 +298,7 @@ reflexivity. induction P;simpl;intros. rewrite ring_morphism_mul. try reflexivity. simpl. Esimpl. rewrite IHP1;rewrite IHP2;rsimpl. - repeat rewrite phiCR_comm. Esimpl. Qed. + Qed. Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c]. Proof. @@ -618,4 +618,4 @@ exact pow_th. apply Peq_ok;trivial. Qed. -End MakeRingPol.
\ No newline at end of file +End MakeRingPol. |