diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-14 11:45:26 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-14 11:45:26 +0000 |
| commit | 5a3ea72512746ffbe452296ee5e194b69f029b33 (patch) | |
| tree | 2c8685652a276acafe87da1ba095cad046e1fbb9 /plugins/micromega | |
| parent | 28000ead7870114795b21b3cc819aadc4dab329d (diff) | |
More newlines in debugging output of psatzl
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14902 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 1ad49bb8c..be49aa351 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -895,7 +895,9 @@ struct let parse_expr parse_constant parse_exp ops_spec env term = if debug then (Pp.pp (Pp.str "parse_expr: "); - Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ()); + Pp.pp (Printer.prterm term); + Pp.pp (Pp.str "\n"); + Pp.pp_flush ()); (* let constant_or_variable env term = @@ -1009,10 +1011,12 @@ struct if debug then (Pp.pp_flush (); Pp.pp (Pp.str "rconstant: "); - Pp.pp (Printer.prterm term); Pp.pp_flush ()); + Pp.pp (Printer.prterm term); + Pp.pp (Pp.str "\n"); + Pp.pp_flush ()); let res = rconstant term in if debug then - (Printf.printf "rconstant -> %a" pp_Rcst res ; flush stdout) ; + (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; res @@ -1052,6 +1056,7 @@ struct then (Pp.pp_flush (); Pp.pp (Pp.str "parse_arith: "); Pp.pp (Printer.prterm cstr); + Pp.pp (Pp.str "\n"); Pp.pp_flush ()); match kind_of_term cstr with | App(op,args) -> |