]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
- Procedural: new flag "level=n" to control the reconstruction level (defaults to...
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index e2ab011dac927cd33a05c4c741240a9c8766ed36..ecdee9f7bd9a80be1e1dc1909e9595bfa0750c63 100644 (file)
@@ -453,10 +453,11 @@ EXTEND
   inline_params:[
    [ params = LIST0 
       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix  
-      | IDENT "procedural" -> G.IPProcedural
       | flavour = inline_flavour -> G.IPAs flavour
-      | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth 
+      | IDENT "procedural" -> G.IPProcedural
       | IDENT "nodefaults" -> G.IPNoDefaults
+      | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth 
+      | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level 
       ] -> params
    ]
 ];