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...