]> 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 633d98ea9d69bece6e5c6de070adbdc8be59269f..5a22a4b62817c6cf354d9bcfa7668aa03deacff7 100644 (file)
@@ -436,7 +436,6 @@ EXTEND
    | IDENT "timeout"
    | IDENT "library"
    | IDENT "type"
-   | IDENT "steps"
    | IDENT "all"
    ]
 ];
@@ -629,10 +628,12 @@ EXTEND
         let rex = Str.regexp ("^"^ident^"$") in
         if Str.string_match rex id 0 then
           if (try ignore (UriManager.uri_of_string uri); true
-              with UriManager.IllFormedUri _ -> false)
+              with UriManager.IllFormedUri _ -> false) ||
+             (try ignore (NReference.reference_of_string uri); true
+              with NReference.IllFormedReference _ -> false)
           then
             L.Ident_alias (id, uri)
-          else 
+          else
             raise
              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
         else
@@ -793,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)