C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonymous,so,type_of_branch ~subst
+ C.Prod (name,so,type_of_branch ~subst
((Some (name,(C.Decl so)))::context) argsno need_dummy
(CicSubstitution.lift 1 outtype) term' de)
- | _ -> raise (AssertFailure (lazy "20"))
+ | _ -> raise (AssertFailure (lazy "20"))
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
type_of_aux ~logger
((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
in
- (CicSubstitution.subst s ty1),ugraph2
+ (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
| C.Appl (he::tl) when List.length tl > 0 ->
let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
let tlbody_and_type,ugraph2 =
R.are_convertible
~subst ~metasenv context ty_p ty_branch ugraph3
in
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
if not b1 then
debug_print (lazy
("#### " ^ CicPp.ppterm ty_p ^
begin
CicReduction.fdebug := -1 ;
eat_prods ~subst context
- (CicSubstitution.subst hete t) tl ugraph1
+ (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+ tl ugraph1
(*TASSI: not sure *)
end
else
(** wrappers which instantiate fresh loggers *)
+let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
+
let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
- type_of_aux' ~logger ~subst metasenv context t ugraph
+ profiler.HExtlib.profile
+ (type_of_aux' ~logger ~subst metasenv context t) ugraph
let typecheck_obj uri obj =
let logger = new CicLogger.logger in