X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fgallina8Parser.mly;h=e72dbbf3036795ed23e2fcd7c75f135b102a25b3;hb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;hp=8bba4fb0bbb33d30e4ebcd5ffc2e804506d1e432;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly
index 8bba4fb0b..e72dbbf30 100644
--- a/helm/software/components/binaries/transcript/gallina8Parser.mly
+++ b/helm/software/components/binaries/transcript/gallina8Parser.mly
@@ -37,7 +37,7 @@
 
    let mk_vars local idents =
       let kind = if local then T.Var else T.Con in
-      let map ident = T.Inline (local, kind, trim ident, "", None) in
+      let map ident = T.Inline (local, kind, trim ident, "", None, []) in
       List.map map idents
 
    let strip2 s =
@@ -65,7 +65,7 @@
         | _            -> assert false
 
    let mk_morphism ext =
-      let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in
+      let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem, []) in
       List.rev_map generate ["2"; "1"]
 
 %}
@@ -297,25 +297,25 @@
    macro_step:
       | th ident opt_lskips def xskips FS
          { out "TH" $2;
-	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
 	 }
       | th ident lskips fs just FS 
          { out "TH" $2;
-	   $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	   $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
 	 }
       | gen ident def xskips FS
          { out "TH" $2;
-	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
 	 }      
       | mor ident cn ident fs just FS
          { out "MOR" $4; $6 @ mk_morphism (trim $4)                 }
       | xlet ident opt_lskips def xskips FS
          { out "TH" $2;
-	   [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	   [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])]
 	 }
       | xlet ident lskips fs just FS 
          { out "TH" $2;
-	   $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	   $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])]
 	 }
       | var idents cn xskips FS
          { out "VAR" (cat $2); mk_vars true $2                      }
@@ -323,7 +323,7 @@
          { out "AX" (cat $2); mk_vars false $2                      }
       | ind ident skips FS
          { out "IND" $2;
-	   T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
+	   T.Inline (false, T.Ind, trim $2, "", None, []) :: snd $3
 	 }
       | sec ident FS
          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
@@ -332,11 +332,11 @@
       | unx xskips FS
          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
       | req xp ident FS
-         { out "REQ" $3; [T.Include (trim $3)]                      }
+         { out "REQ" $3; [T.Include (true, trim $3)]               }
       | req ident FS
-         { out "REQ" $2; [T.Include (trim $2)]                      } 
+         { out "REQ" $2; [T.Include (true, trim $2)]               } 
       | load str FS
-         { out "REQ" $2; [T.Include (strip2 (trim $2))]             }
+         { out "REQ" $2; [T.Include (true, strip2 (trim $2))]      }
       | coerc qid spcs skips FS
          { out "COERCE" (hd $2); coercion (hd $2)                   }
       | id coerc qid spcs skips FS