Implicit annotationas are now printed

[helm.git] / helm / software / components / binaries / transcript / v8Parser.mly

diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly
index 52456c5594d761957d7d3576683952dd975b3ddb..721cdd14109f1b3dcd21dfa7f98c07f0e15bc819 100644 (file)
--- a/helm/software/components/binaries/transcript/v8Parser.mly
+++ b/helm/software/components/binaries/transcript/v8Parser.mly
@@ -25,8 +25,9 @@
 
 %{
    module T = Types
-   
-   let out t s = prerr_endline ("-- " ^ t ^ " " ^ s)
+   module O = Options
+
+   let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s)
 
    let trim = HExtlib.trim_blanks
 
@@ -58,6 +59,7 @@
         | "Theorem"    -> Some `Theorem
         | "Definition" -> Some `Definition
         | "Fixpoint"   -> Some `Definition
+        | "CoFixpoint" -> Some `Definition
         | "Let"        -> Some `Definition
        | "Scheme"     -> Some `Theorem
         | _            -> assert false