"include" command implemented.

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 86c7185ecf1308d75e1f34707059c1cc77f3fc1f..3a8b5213c805484e4bf9b36249244cfe19cfe3d1 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -220,6 +220,7 @@ let pp_obj = function
 
 
 let pp_command = function
+  | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
   | Drop _ -> "drop"
   | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value