]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
freescale porting, work in progress
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 8fbe6b8d1c709b84dc995fd6bb020e3603346927..eddac97464f4e0b595d0fe7fbe4c17d297f31d6e 100644 (file)
@@ -360,7 +360,15 @@ let pp_ncommand = function
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
   | NObj (_,_)
   | 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