diff options
| author | Frédéric Besson | 2019-05-14 14:54:22 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-05-22 11:08:42 +0200 |
| commit | 551552aeb9ae5f04fbd9b71d1d00c6059090c052 (patch) | |
| tree | 4334d8a0b57170a60502c2f6df9d8d2cb7e4cbf8 /plugins/omega | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Partly revert micromega parsing using typeclasses.
Typeclasses resolution is not used anymore for lia.
Typeclasses resolution is still used by lra but only to access a
database of declared constants.
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) |