[Git][monnier/typer][unification] 3 commits: fixing db issue when calling OL.lexp_whnf
Stefan pushed to branch unification at Stefan / Typer Commits: 4ea22894 by Pierre Delaunay at 2016-11-08T11:38:22-05:00 fixing db issue when calling OL.lexp_whnf - - - - - 3502c27e by Pierre Delaunay at 2016-11-08T11:38:59-05:00 Merge branch 'master' of gitlab.com:monnier/typer - - - - - 015fdd7e by Stefan Monnier at 2016-11-08T14:20:15-05:00 Merge branch 'trunk' into unification - - - - - 1 changed file: - src/lparse.ml Changes: ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -690,16 +690,16 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* Extract correct ordering aargs: all args and eargs: explicit args. *) let meta_ctx, _ = !global_substitution in - let rec extract_order ltp aargs eargs = - match OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx with + let rec extract_order ltp aargs eargs nctx = + match OL.lexp_whnf ltp nctx meta_ctx with | Arrow (kind, Some (_, varname), ltp, _, ret) -> extract_order ret ((kind, varname, ltp)::aargs) - (if kind = Aexplicit then (varname::eargs) else eargs) + (if kind = Aexplicit then (varname::eargs) else eargs) (lctx_extend nctx None (ForwardRef) ltp) | e -> (List.rev aargs), List.rev eargs in (* First list has all the arguments, second only holds explicit arguments. *) - let order, eorder = extract_order ltp [] [] in + let order, eorder = extract_order ltp [] [] (ectx_to_lctx ctx) in (* print_string "Type :"; lexp_print ltp; print_string "\n"; View it on GitLab: https://gitlab.com/monnier/typer/compare/e66bcd5bf66f8f21c3f9a8ef7546246c996...
Afficher les réponses par date
participants (1)
-
Stefan