X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=06d4d908ba2fd7d9c49e8794e4d413a222279dff;hb=62e3a3ce3ac21ab25074ad2af1883a4b0cbc62be;hp=61413e7fe0089a91b77f26866465e897869dc9e1;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly
index 61413e7fe..06d4d908b 100644
--- a/components/binaries/transcript/v8Parser.mly
+++ b/components/binaries/transcript/v8Parser.mly
@@ -43,6 +43,12 @@
 
    let strip1 s = 
       String.sub s 1 (String.length s - 1)
+
+   let coercion str = 
+      [T.Coercion (false, str); T.Coercion (true, str)]
+
+   let notation str =
+      [T.Notation (false, str); T.Notation (true, str)]
 %}
    %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
    %token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
@@ -189,9 +195,9 @@
    ;
    field: 
       | ident cn unexports_r  
-         { $1 ^ $2 ^ fst $3, snd $3                          }
+         { $1 ^ $2 ^ fst $3, snd $3                      }
       | ident coe unexports_r 
-         { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion (trim $1)] }
+         { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
    ;  
    fields:
       | field           { $1                                      }
@@ -269,9 +275,9 @@
       | load str FS
          { out "REQ" $2; [T.Include (strip2 (trim $2))]             }
       | coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $2); [T.Coercion (hd $2)]               }
+         { out "COERCE" (hd $2); coercion (hd $2)                   }
       | id coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $3); [T.Coercion (hd $3)]               }
+         { out "COERCE" (hd $3); coercion (hd $3)                   }
       | th ident error 
          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
       | ind ident error 
@@ -284,7 +290,7 @@
       | OQ verbatims CQ       { [T.Comment $2]                       }
       | macro_step            { $1                                   }
       | set unexports FS      { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
-      | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ trim $3)] }
+      | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3)     }
       | error                 { out "ERROR" "item"; failwith "item"  }
     ;
     items: