diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 09:44:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 09:44:31 +0000 |
| commit | 9a57002cd644bac29e0ad338756d1a01613e6c13 (patch) | |
| tree | 59ea332f070aef67b4256a8dc642a2fd66dcc451 | |
| parent | 536407d31295258a5b5d40514f55744fd58203ea (diff) | |
small copy&paste bug in zify: some Pmult should be Nmult
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10301 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/omega/PreOmega.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/omega/PreOmega.v b/contrib/omega/PreOmega.v index 0a4328497..47e22a97f 100644 --- a/contrib/omega/PreOmega.v +++ b/contrib/omega/PreOmega.v @@ -412,12 +412,12 @@ Ltac zify_N_op := | |- context [ Z_of_N (Nsucc ?a) ] => rewrite (Z_of_N_succ a) (* Nmult -> Zmult and a positivity hypothesis *) - | H : context [ Z_of_N (Pmult ?a ?b) ] |- _ => + | H : context [ Z_of_N (Nmult ?a ?b) ] |- _ => let H:= fresh "H" in - assert (H:=Z_of_N_le_0 (Pmult a b)); rewrite (Z_of_N_mult a b) in * - | |- context [ Z_of_N (Pmult ?a ?b) ] => + assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * + | |- context [ Z_of_N (Nmult ?a ?b) ] => let H:= fresh "H" in - assert (H:=Z_of_N_le_0 (Pmult a b)); rewrite (Z_of_N_mult a b) in * + assert (H:=Z_of_N_le_0 (Nmult a b)); rewrite (Z_of_N_mult a b) in * (* atoms of type N : we add a positivity condition (if not already there) *) | H : context [ Z_of_N ?a ] |- _ => |