]> matita.cs.unibo.it Git - helm.git/commitdiff
added `Coer print_kind
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 13:45:36 +0000 (13:45 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Feb 2005 13:45:36 +0000 (13:45 +0000)
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