From 551552aeb9ae5f04fbd9b71d1d00c6059090c052 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Tue, 14 May 2019 14:54:22 +0200
Subject: 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.
---
 plugins/omega/PreOmega.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'plugins/omega')

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)
-- 
cgit v1.2.3