]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
more tests
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index 324231b50db3e0bdc9655036535acc93f9f8fbe1..5a22a4b62817c6cf354d9bcfa7668aa03deacff7 100644 (file)
@@ -436,7 +436,6 @@ EXTEND
    | IDENT "timeout"
    | IDENT "library"
    | IDENT "type"
-   | IDENT "steps"
    | IDENT "all"
    ]
 ];
@@ -795,8 +794,10 @@ EXTEND
         indty = tactic_term; paramspec = inverter_param_list ->
           G.Inverter
             (loc, name, indty, paramspec)
-            | IDENT "record" ; (params,name,ty,fields) = record_spec ->
+    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.Obj (loc, N.Record (params,name,ty,fields))
+    | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+        G.NObj (loc, N.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         G.Default (loc,what,uris)