Salut Vincent,
- -let elab_check_sort (ctx : elab_context) lsort (l, name) ltp = - match OL.lexp_whnf lsort (ectx_to_lctx ctx) VMap.empty with - | Sort (_, _) -> () (* All clear! *) - | _ -> lexp_error l ("Type of `" ^ name ^ "` is not a proper type: " - ^ lexp_to_str ltp) - -let elab_check_proper_type (ctx : elab_context) ltp v = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) v ltp - with e -> print_string ("Exception while checking type `" - ^ lexp_to_str ltp ^ "` of var `" ^ - (let (_, name) = v in name) ^"`\n"); - print_lexp_ctx (ectx_to_lctx ctx); - raise e - -let elab_check_def (ctx : elab_context) var lxp ltype = - let lctx = ectx_to_lctx ctx in - if OL.conv_p ltype (OL.check lctx lxp) then - elab_check_proper_type ctx ltype var +let elab_check_def (ctx : lexp_context) var lxp ltype = + if OL.conv_p ltype (OL.check ctx lxp) then + () (* FIXME: Check ltype as well! *) else (print_string "¡¡ctx_define error!!\n"; lexp_print lxp; print_string " !: "; lexp_print ltype; print_string "\nbecause\n"; - lexp_print (OL.check lctx lxp); + lexp_print (OL.check ctx lxp); print_string " != "; lexp_print ltype; print_string "\n"; lexp_fatal (let (l,_) = var in l) "TC error")
Hmm... ça c'est l'exact inverse de ce que j'ai installé hier. Aurais-tu fait une erreur de manipulation par hasard? SVP vérifie le diff de ton dernier commit pour t'assurer que c'est bien ce que tu voulais faire. Stefan