From 5ff1fc8b41e8265af7e1c1c91d137ec88f2b04d0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Dec 2018 17:20:41 +0100
Subject: Do not take universes into account in lia reification.

This is slightly blunt, it might be the case that we get delayed constraints
that cannot be solved resulting in a later universe inconsistency, but it looks
highly unlikely on arithmetical statements.

Alternatively we would have threaded the unification state, but this would
have required a much deeper change.

Fixes #9268.
---
 plugins/micromega/coq_micromega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d4bafe773f..7adae148bd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -846,7 +846,7 @@ struct
      match env with
       | [] -> ([v],n)
       | e::l ->
-         if EConstr.eq_constr sigma e v
+         if EConstr.eq_constr_nounivs sigma e v
          then (env,n)
          else
           let (env,n) = _add l ( n+1) v in
-- 
cgit v1.2.3