- Procedural convertible rewrites in the conclusion are now detected and replaced...

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

diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly
index 8bba4fb0bbb33d30e4ebcd5ffc2e804506d1e432..e72dbbf3036795ed23e2fcd7c75f135b102a25b3 100644 (file)
--- 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