]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
...
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 7ececab722b2b5ff61037ed76ea76df4c0276d81..f05cb9595b9bb9676b8631d8a6a941addb5af81c 100644 (file)
@@ -370,8 +370,9 @@ let pp_command ~term_pp ~obj_pp = function
      "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
-  | Include (_,true,path) -> "include \"" ^ path ^ "\""
-  | Include (_,false,path) -> "include source \"" ^ path ^ "\""
+  | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\""
+  | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\""
+  | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path
   | Obj (_,obj) -> obj_pp obj
   | Qed _ -> "qed"
   | Relation (_,id,a,aeq,refl,sym,trans) ->