diff options
| author | Pierre-Marie Pédrot | 2020-04-14 12:24:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-14 12:24:18 +0200 |
| commit | b26d17a6a76b6758d0f22eaa025b1c31b474809f (patch) | |
| tree | f119296a9a545132d81e0a78ade56883968f11d3 /interp | |
| parent | 585884b757b8eef4052ddb45b42b15bfce372c0d (diff) | |
| parent | f6f2433eddde8b4e09f2ef72f43db88892d03620 (diff) | |
Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of explicit applications
Ack-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 && |