Magic fix for disequality simplify exception.

PLTools · Dec 17, 2024 · 9e7f582 · 9e7f582
1 parent 9def363
commit 9e7f582
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/core/Subst.ml b/src/core/Subst.ml
@@ -157,8 +157,12 @@ let unify ?(subsume=false) ?(scope=Term.Var.non_local_scope) env subst x y =
       ~fvar:(fun ((_, subst) as acc) x y ->
         match walk env subst x, walk env subst y with
         | Var x, Var y      ->
-          if Var.equal x y then acc else extend x (Term.repr y) acc
-        | Var x, Value y    -> extend x y acc
+          (* if Var.equal x y then acc else extend x (Term.repr y) acc *)
+         let cmp = Term.Var.compare x y in
+          if cmp < 0 then extend x (Term.repr y) acc
+          else if cmp > 0 then extend y (Term.repr x) acc
+          else acc
+          | Var x, Value y    -> extend x y acc
         | Value x, Var y    -> extend y x acc
         | Value x, Value y  -> helper x y acc
       )