diff options
| author | Gaëtan Gilbert | 2020-03-31 16:53:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-06 14:48:17 +0200 |
| commit | f6f2433eddde8b4e09f2ef72f43db88892d03620 (patch) | |
| tree | 0c55e143224098e049f4b3462dc4bf507a639f85 /interp | |
| parent | 28c031158cee24faf782a7192032e29229aee4d4 (diff) | |
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.
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 && |