aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-22 18:12:36 +0200
committerHugo Herbelin2019-05-22 18:12:36 +0200
commit5c5bd952e9c28c3acf740fcdced03b2b7145076d (patch)
treea56647f099136d571f2f2c6c47ddb31472ef7804 /interp/constrexpr_ops.ml
parent4f2e05f5abc19addc25501281b4cd34ed5e33853 (diff)
parent28dfb113c19f467fdc2b785d1c5a07a42aefa488 (diff)
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalization + cleanups
Reviewed-by: herbelin
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 443473d5b6..bcb2f34377 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
let binder_kind_eq b1 b2 = match b1, b2 with
| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
-| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
- binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+| Generalized (ck1, b1), Generalized (ck2, b2) ->
+ binding_kind_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false