CicTypeChecker.type_of_aux' metasenv context term ugraph
in
let candidates = get_candidates Unification table term in
+ (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
let r =
if subterms_only then
[]
prerr_endline (string_of_int (List.length expansionsl));
prerr_endline (string_of_int (List.length expansionsr));
*)
-(*
- if expansionsl <> [] then prerr_endline "expansionl";
- if expansionsr <> [] then prerr_endline "expansionr";
-*)
List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
@
List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
end
else
match c with
- | Utils.Gt -> (* prerr_endline "GT"; *)
+ | Utils.Gt ->
let big,small,possmall = l,r,Utils.Right in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
List.map