diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-23 16:33:14 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-12 15:15:45 +0200 |
| commit | 83a3abfa7de680f1a3279710e8f84721c32b7668 (patch) | |
| tree | 843fd161e43ec7ba143413131f6b6057bd8acdba /plugins/omega | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/PreOmega.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 6c0e2d776..d301217fa 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -264,8 +264,8 @@ Ltac zify_positive_op := | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) - | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub a b) in H - | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub a b) + | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H + | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) (* Pos.succ -> Z.succ *) | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H |