- mk_intros st script
-
-and proc_proof st = function
- | C.ALambda (_, name, w, t) -> proc_lambda st name w t
- | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t
- | C.ARel _ as what -> proc_rel st what
- | C.AMutConstruct _ as what -> proc_mutconstruct st what
- | C.AAppl (_, hd :: tl) as what -> proc_appl st what hd tl
- | what -> proc_other st what
-
-and proc_bkd_proofs st synth classes ts =
+ mk_intros st what script
+
+and proc_proof st t =
+ let f st =
+ let xtypes, note = match get_inner_types st t with
+ | Some (it, et) -> Some (H.cic it, H.cic et),
+ (Printf.sprintf "\nInferred: %s\nExpected: %s"
+ (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
+ | None -> None, "\nNo types"
+ in
+ let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
+ let note = Pp.ppcontext st.context ^ note in
+ {st with context = context; clears = clears; clears_note = note; }
+ in
+ match t with
+ | C.ALambda (_, name, w, t) -> proc_lambda st name w t
+ | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
+ | C.ARel _ as what -> proc_rel (f st) what
+ | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
+ | C.AConst _ as what -> proc_const (f st) what
+ | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
+ | what -> proc_other (f st) what
+
+and proc_bkd_proofs st synth names classes ts =