}
in
generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ else
+ raise Not_a_proof
| C.ALetIn (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
}
in
generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
- else raise Not_a_proof
+ else
+ raise Not_a_proof
| C.AAppl (id,li) ->
(try coercion
seed li ~ids_to_inner_types ~ids_to_inner_sorts