- 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 b51a3d76ee62b29d3e84c99868802c6d894bdab8..e72dbbf3036795ed23e2fcd7c75f135b102a25b3 100644 (file)
--- a/helm/software/components/binaries/transcript/gallina8Parser.mly
+++ b/helm/software/components/binaries/transcript/gallina8Parser.mly
@@ -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 (false, trim $3)]               }
+         { out "REQ" $3; [T.Include (true, trim $3)]               }
       | req ident FS
-         { out "REQ" $2; [T.Include (false, trim $2)]               } 
+         { out "REQ" $2; [T.Include (true, trim $2)]               } 
       | load str FS
-         { out "REQ" $2; [T.Include (false, 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