Stefan pushed to branch unification at Stefan / Typer

Commits: f4010f96 by Stefan Monnier at 2016-10-31T12:46:11-04:00 * lparse.ml: Move Pmetavar from infer to check

- - - - -

1 changed file:

- src/lparse.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -363,16 +363,11 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =

Cons(idt, sym), cons_type

- | Pmetavar _ - -> let t = mkMetatype () in - let e = mkMetavar t in - (e, t) - | Phastype (_, pxp, ptp) -> let ltp = lexp_type_infer ptp ctx None trace in (_lexp_p_check pxp ltp ctx trace), ltp

- | (Plambda _ | Pcase _) + | (Plambda _ | Pcase _ | Pmetavar _) -> let t = mkMetatype () in let lxp = _lexp_p_check p t ctx trace in (lxp, t) @@ -454,6 +449,8 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp = (* FIXME: Handle *macro* pcalls here! *) (* | Pcall (fname, _args) -> *)

+ | Pmetavar _ -> mkMetavar t + | _ -> lexp_p_infer_and_check p ctx t trace

and lexp_p_infer_and_check pexp ctx t i =

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