From 9a57002cd644bac29e0ad338756d1a01613e6c13 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 8 Nov 2007 09:44:31 +0000 Subject: 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 --- contrib/omega/PreOmega.v | 8 ++++---- 1 file 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 ] |- _ => -- cgit v1.2.3