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/micromega/DeclConstant.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/micromega/DeclConstant.v')

diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v
index 47fcac6481..4e8fe5a8ff 100644
--- a/plugins/micromega/DeclConstant.v
+++ b/plugins/micromega/DeclConstant.v
@@ -62,6 +62,7 @@ Instance DZO: DeclaredConstant Z0 := {}.
 Instance DZpos: DeclaredConstant Zpos := {}.
 Instance DZneg: DeclaredConstant Zneg := {}.
 Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}.
+Instance DZpow     : DeclaredConstant Z.pow     := {}.
 
 Require Import QArith.
 
-- 
cgit v1.2.3