diff options
| author | ppedrot | 2012-06-01 20:08:33 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 20:08:33 +0000 |
| commit | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (patch) | |
| tree | ec5246ac1cfc741dc30c33fe6551216dfdef6a54 /plugins/funind/functional_principles_proofs.ml | |
| parent | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (diff) | |
More cleaning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fd9c09c..b8887c68f9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -23,23 +23,15 @@ open Misctypes (* let observe strm = if do_observe () - then Pp.msgnl strm - else () - -let observennl strm = - if do_observe () - then begin Pp.msg strm;Pp.pp_flush () end + then Pp.msg_debug strm else () - - - let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> let e = Cerrors.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in - msgnl (str "observation "++ s++str " raised exception " ++ + msg_debug (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); raise e;; |