let eqterm =
C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
let gproof, gmetas, gterm = goal in
- debug_print
- (lazy
- (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
- (string_of_equality equality) (CicPp.ppterm gterm)));
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *)
+(* (string_of_equality equality) (CicPp.ppterm gterm))); *)
try
let subst, metasenv', _ =
let menv = metasenv @ metas @ gmetas in
in
let r, s, l =
if Inference.term_is_equality term then
- let _ = debug_print (lazy "OK, is equality!!") in
+(* let _ = debug_print (lazy "OK, is equality!!") in *)
let rec appleq_a = function
| [] -> false, [], []
| (Positive, equality)::tl ->