Indentation
This commit is contained in:
parent
73984f4232
commit
29d7e67a00
9
main.ml
9
main.ml
@ -135,16 +135,11 @@ while !subgoals <> [] do
|
|||||||
done;
|
done;
|
||||||
|
|
||||||
let finalLam = !fill_holes [] in
|
let finalLam = !fill_holes [] in
|
||||||
if (typecheck [] finalLam ty)
|
if (typecheck [] finalLam ty) then
|
||||||
then
|
|
||||||
Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
|
Printf.printf "Final proof :\n%s\n" (string_of_lam finalLam)
|
||||||
else
|
else (
|
||||||
(
|
|
||||||
Printf.printf "Invalid proof constructed !\n";
|
Printf.printf "Invalid proof constructed !\n";
|
||||||
Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
|
Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
|
||||||
Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
|
Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
|
||||||
)
|
)
|
||||||
;;
|
;;
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user