]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/text/txtParser.mly
notational update in lambdadelta completed
[helm.git] / helm / software / helena / src / text / txtParser.mly
index d08fb87d9ede95119ffdab5c7ce44a1ee2e608f0..32a0decaf721f8cce9dc43ef7843dc504668c7e6 100644 (file)
    module G  = Options
    module N  = Layer
    module T  = Txt
-   
+
+IFDEF PARSER THEN   
    let _ = Parsing.set_trace !G.debug_parser
+END
 %}
    %token <int> IX
    %token <string> ID STR
@@ -68,7 +70,7 @@
       | sort CM sorts { $1 :: $3 }
    ;
    layer:
-      |       { N.infinite  }
+      |       { N.infinity  }
       | CT IX { N.finite $2 }
    ;