- try
- let _ = CicTypeChecker.type_of_aux' [] [] expr in
- ProofEngine.proof :=
- Some (UriManager.uri_of_string "cic:/dummy.con",
- [1,expr], Cic.Meta 1, expr) ;
- ProofEngine.goal := Some (1,([],expr)) ;
- refresh_sequent proofw ;
- refresh_proof output ;
- with
- e ->
- print_endline ("? " ^ CicPp.ppterm expr) ;
- raise e
+ let _ = CicTypeChecker.type_of_aux' [] [] expr in
+ ProofEngine.proof :=
+ Some (UriManager.uri_of_string "cic:/dummy.con",
+ [1,expr], Cic.Meta 1, expr) ;
+ ProofEngine.goal := Some (1,([],expr)) ;
+ refresh_sequent proofw ;
+ refresh_proof output ;