]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/v8Parser.mly
- transcript: now outputs includes and coercions correctly
[helm.git] / helm / software / components / binaries / transcript / v8Parser.mly
index 7fd69615d5537be513df8bda2304b88fa0807d6a..61413e7fe0089a91b77f26866465e897869dc9e1 100644 (file)
@@ -91,7 +91,6 @@
    id: ID spcs { $1 ^ $2 };
    coerc: COERC spcs { $1 ^ $2 };
 
-
    idents:
       | ident        { [$1]     }
       | ident idents { $1 :: $2 }
       | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } 
    ;
    field: 
-      | ident cn unexports_r  { $1 ^ $2 ^ fst $3, snd $3                   }
-      | ident coe unexports_r { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion $1] }
+      | ident cn unexports_r  
+         { $1 ^ $2 ^ fst $3, snd $3                          }
+      | ident coe unexports_r 
+         { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion (trim $1)] }
    ;  
    fields:
       | field           { $1                                      }
       | var idents xres FS
          { out "VAR" (cat $2); mk_vars $2                           }      
       | ind ident unexports FS
-         { out "IND" $2; snd $3 @ [T.Inline (T.Ind, trim $2)]       }
+         { out "IND" $2; T.Inline (T.Ind, trim $2) :: snd $3        }
       | sec unexports FS 
          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
       | req xp ident FS