diff options
| author | herbelin | 2003-11-14 16:28:10 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-14 16:28:10 +0000 |
| commit | cf7b845b433ea0aeb97430093c51ec77c3d1c4af (patch) | |
| tree | 864f4a1897a9844f0fb812c01e909162eeddd733 | |
| parent | cf8259ccd6383366bcb324d67e6df7d1c768cacc (diff) | |
Check bavard meme en mode silencieux, car on l'a voulu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4909 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5b84e9311f..94bdb1a083 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -828,12 +828,12 @@ let vernac_check_may_eval redexp glopt rc = match redexp with | None -> if !pcoq <> None then (out_some !pcoq).print_check j - else Options.if_verbose msg (print_judgment env j) + else msg (print_judgment env j) | Some r -> let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in if !pcoq <> None then (out_some !pcoq).print_eval (redfun env evmap) env rc j - else Options.if_verbose msg (print_eval redfun env j) + else msg (print_eval redfun env j) (* The same but avoiding the current goal context if any *) let vernac_global_check c = |