added Variant theorem flavour

[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 bd26fb387492dcc6947b23945d7769a2bd64a03b..794e09e708cbf517b418be743b9899e44c3bab62 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -141,12 +141,14 @@ let pp_flavour = function
   | `Lemma -> "Lemma"
   | `Remark -> "Remark"
   | `Theorem -> "Theorem"
+  | `Variant -> "Variant"
 
 let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"
   | `Elim -> "elim"
+  | `Instance -> "instance"
 
 let pp_macro pp_term = function 
   (* Whelp *)
@@ -227,7 +229,6 @@ let pp_obj = function
     "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
     pp_fields fields ^ "}"
 
-
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"