]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
ncopy partially implemented and fixed (a ?) chain to print elimintaors
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 2cd7a4f4fcddfee286d115b84ff79c5a18cee9ad..eddac97464f4e0b595d0fe7fbe4c17d297f31d6e 100644 (file)
@@ -362,6 +362,13 @@ let pp_ncommand = function
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
   | NQed (_) -> "nqed"
+  | NCopy (_,name,uri,map) -> 
+      "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
+        String.concat " and " 
+          (List.map 
+            (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) 
+            map)
+;;
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri