diff options
| author | pboutill | 2011-06-10 18:34:49 +0000 |
|---|---|---|
| committer | pboutill | 2011-06-10 18:34:49 +0000 |
| commit | 7b80c5023071a0dead641da1d14078489f6e6f4c (patch) | |
| tree | b51d714d85937ba2281244dea1d913bcef055b3c /parsing/printer.mli | |
| parent | 2856df4134047a06df13f5cff3d8c62158c03779 (diff) | |
Revert "Check if recursive calls are guarded before printing "Proof completed"."
because guard condition is checked at Qed anyway and it can be expensivise to
check it twice. Use explicitly "Guarded" if you want this information.
But the wrong proof completed is now the right no more subgoals ...
Of course, we would like an incrementally checked guard condition one
day !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14177 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.mli')
| -rw-r--r-- | parsing/printer.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 3a5c3decae..cdd2f42770 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -104,7 +104,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds +val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -138,7 +138,7 @@ val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds type printer_pr = { - pr_subgoals : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds; + pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; |