- let names =
- List.map (function None -> None | Some (x,_) -> Some x) context
- in
- prerr_endline ("PROOF:" ^ CicPp.pp proof names);
- prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
- prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
- prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
- end;
- assert b
+ let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+ let b,_ = CicReduction.are_convertible context ty goalty u in
+ if not b then
+ begin
+ let names =
+ List.map (function None -> None | Some (x,_) -> Some x) context
+ in
+ prerr_endline ("PROOF:" ^ CicPp.pp proof names);
+ prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
+ prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
+ prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ end;
+ assert b
+ end
+ else ()