diff options
| author | Vincent Laporte | 2019-05-22 11:53:02 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-22 11:53:02 +0000 |
| commit | 2744d61704e2fdd96bdc2c60c9d7f7af8367f4d4 (patch) | |
| tree | 0058f6fb70cf1d80b11e46f46753ff2550348672 /plugins/omega | |
| parent | e7d03413c6b8f8fbcc537a43da4c3f9ff19007ad (diff) | |
| parent | 551552aeb9ae5f04fbd9b71d1d00c6059090c052 (diff) | |
Merge PR #10207: Partly revert micromega parsing using typeclasses.
Reviewed-by: vbgl
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/PreOmega.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 695f000cb1..23d7b141a4 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -359,7 +359,10 @@ Ltac zify_positive_rel := Ltac zify_positive_op := match goal with - (* Zneg -> -Zpos (except for numbers) *) + (* Z.pow_pos -> Z.pow *) + | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H + | |- context [ Z.pow_pos ?a ?b ] => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) + (* Zneg -> -Zpos (except for numbers) *) | H : context [ Zneg ?a ] |- _ => let isp := isPcst a in match isp with @@ -377,6 +380,10 @@ Ltac zify_positive_op := | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Z.power_pos *) + | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H + | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Pos.add -> Z.add *) | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) |