]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
ncopy partially implemented and fixed (a ?) chain to print elimintaors
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index dfef4d237a0ea34c8883b2b23b1e734fb46b8fcd..5ed2939488b82f7355296f08a26c01a3686f52c2 100644 (file)
@@ -836,6 +836,10 @@ EXTEND
           G.NCoercion(loc,name,t,ty,(id,source),target)     
     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
+    | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with"; 
+      m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
+        G.NCopy (loc,s,NUri.uri_of_string u,
+          List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
   ]];
 
   grafite_command: [ [