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.

2 files changed, 47 insertions, 1 deletions

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
diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v
new file mode 100644
index 0000000000..02dd46f6d2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9268.v
@@ -0,0 +1,46 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+
+Local Open Scope Z_scope.
+
+Definition Register := Z%type.
+
+Definition Opcode := Z%type.
+
+Inductive InstructionI : Type
+  := Lb : Register -> Register -> Z -> InstructionI
+  |  InvalidI : InstructionI.
+
+Inductive Instruction : Type
+  := IInstruction : InstructionI -> Instruction.
+
+Definition funct3_LB : Z := 0.
+
+Definition opcode_LOAD : Opcode := 3.
+
+Set Universe Polymorphism.
+
+Definition MachineInt := Z.
+
+Definition funct3_JALR := 0.
+
+Axiom InstructionMapper: Type -> Type.
+
+Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z :=
+  match inst with
+  | IInstruction   InvalidI   => 2
+  | IInstruction   (Lb  rd rs1 oimm12) => 3
+   end.
+
+Axiom Encoder: InstructionMapper MachineInt.
+
+Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder.
+
+Lemma foo: forall (ins: InstructionI),
+    0 <= encode (IInstruction ins) ->
+    0 <= encode (IInstruction ins) .
+Proof.
+  Set Printing Universes.
+  intros.
+  lia.
+Qed.