[Micromega] Use EConstr.eq_constr_universes_proj

3 files changed, 45 insertions, 5 deletions

diff --git a/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst
new file mode 100644
index 0000000000..d6fc724415
--- /dev/null
+++ b/doc/changelog/04-tactics/10806-fix-micromega-wrt-projections.rst
@@ -0,0 +1,4 @@
+- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by
+  primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_,
+  fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
+  by Vincent Laporte).
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ceb651abed..8ca7b48a32 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -745,7 +745,7 @@ struct
     (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *)
     let eq_constr gl x y =
       let evd = gl.sigma in
-      match EConstr.eq_constr_universes gl.env evd x y with
+      match EConstr.eq_constr_universes_proj gl.env evd x y with
       | Some csts ->
          let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
          begin
@@ -769,15 +769,16 @@ struct
     ({vars=vars';gl=gl'}, CamlToCoq.positive n)
 
    let get_rank env v =
-     let evd = env.gl.sigma in
+     let gl = env.gl in
 
      let rec _get_rank env n =
        match env with
        | [] -> raise (Invalid_argument "get_rank")
       | e::l ->
-         if EConstr.eq_constr evd e v
-         then n
-         else  _get_rank l (n+1)  in
+        match eq_constr gl e v with
+        | Some _ -> n
+        | None -> _get_rank l (n+1)
+     in
      _get_rank env.vars 1
 
    let elements env = env.vars
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
new file mode 100644
index 0000000000..25285622a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -0,0 +1,35 @@
+Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+
+Set Primitive Projections.
+Record params := { width : Z }.
+Definition p : params := Build_params 64.
+
+Set Printing All.
+
+Goal width p = 0%Z -> width p = 0%Z.
+  intros.
+
+  assert_succeeds (enough True; [omega|]).
+  assert_succeeds (enough True; [lia|]).
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  change tt with tt in H.
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  assert_succeeds (enough True; [lia|]).
+  (* Tactic failure: <tactic closure> fails. *)
+  (* assert_succeeds (enough True; [omega|]). *)
+  (* Tactic failure: <tactic closure> fails. *)
+
+  (* omega. *)
+  (* Error: Omega can't solve this system *)
+
+  lia.
+  (* Tactic failure:  Cannot find witness. *)
+Qed.