]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAst.ml
added `Coer print_kind
[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml
index ed8e4ec6e8aeee0920be3c39cc44ebe5ba40f9bb..eae88a14d279ee8852ff13963950f1fd43a69777 100644 (file)
@@ -90,7 +90,7 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
-type print_kind = [ `Env ]
+type print_kind = [ `Env | `Coer ]
 
 type 'term command =
   | Abort