Commit 81b34ace authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use the Proof keyword in Coq printer.

parent 07132f83
......@@ -604,12 +604,11 @@ let intros fmt fmla =
let print_empty_proof fmt def =
match def with
| Some (_params,fmla) ->
fprintf fmt "Proof.@\n";
if need_intros fmla then intros fmt fmla;
fprintf fmt "@\n@\n";
fprintf fmt "Qed.@\n"
fprintf fmt "@\n@\nQed.@\n"
| None ->
fprintf fmt "@\n";
fprintf fmt "Defined.@\n"
fprintf fmt "Proof.@\n@\nDefined.@\n"
let print_previous_proof def info fmt previous =
match previous with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment