From f6f2433eddde8b4e09f2ef72f43db88892d03620 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Mar 2020 16:53:42 +0200
Subject: Fix #11934 equality on constrexpr ignores instances of explicit
 applications

While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
---
 interp/constrexpr_ops.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d4369e9bd1..d6097304ec 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -121,9 +121,10 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
-    | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
+    | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
       qualid_eq r1 r2 &&
+      eq_universes u1 u2 &&
       List.equal constr_expr_eq al1 al2
     | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
@@ -158,8 +159,8 @@ let rec constr_expr_eq e1 e2 =
       Id.equal id1 id2 && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
       Glob_ops.glob_sort_eq s1 s2
-  | CCast(t1,c1), CCast(t2,c2) ->
-    constr_expr_eq t1 t2 && cast_expr_eq c1 c2
+    | CCast(t1,c1), CCast(t2,c2) ->
+      constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
       Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
       notation_eq n1 n2 &&
-- 
cgit v1.2.3