X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=8bba4fb0bbb33d30e4ebcd5ffc2e804506d1e432;hb=84e770b58ae08a345087de816aba29bc2fc727ba;hp=52456c5594d761957d7d3576683952dd975b3ddb;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git

diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly
index 52456c559..8bba4fb0b 100644
--- 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
@@ -98,10 +100,7 @@
    ind: IND spcs { $1 ^ $2 };
    set: SET spcs { $1 ^ $2 };
    notation: NOT spcs { $1 ^ $2 };
-   oc: OC spcs { $1 ^ $2 };
-   coe: COE spcs { $1 ^ $2 };
    cn: CN spcs { $1 ^ $2 };
-   sc: SC spcs { $1 ^ $2 };
    str: STR spcs { $1 ^ $2 };
    id: ID spcs { $1 ^ $2 };
    coerc: COERC spcs { $1 ^ $2 };
@@ -370,6 +369,10 @@
 
 
 /*
+   oc: OC spcs { $1 ^ $2 };
+   coe: COE spcs { $1 ^ $2 };
+   sc: SC spcs { $1 ^ $2 };
+
    cnot:
       | EXTRA { $1 }
       | INT   { $1 }