Stefan pushed to branch unification at Stefan / Typer

Commits: 293f20f6 by Stefan Monnier at 2016-07-28T14:15:34-04:00 * tests/inverse_test.ml (is_identity.is_identity): Forget it

* src/lexp.ml (push_susp): Don't be so picky.

- - - - -

2 changed files:

- src/lexp.ml - tests/inverse_test.ml

Changes:

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -328,10 +328,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp * rather than Susp. *) - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; + | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) push_susp e (scompose s' s) | (Var _ | Metavar _) - -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; + -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) push_susp (mkSusp e s) S.identity

let nosusp e = (* Return `e` without `Susp`. *)

===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -56,7 +56,7 @@ let is_identity s = let rec is_identity s acc = match s with | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> (0 = shift) + | S.Shift(S.Identity, shift) -> (acc = shift) | S.Identity -> true | _ -> false in is_identity s 0

View it on GitLab: https://gitlab.com/monnier/typer/commit/293f20f65d551488bcf599af7c2bd8536c7e...