X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateTypes.mli;h=58458d1ffa5d008618755828d766ae2ed454bbb1;hp=523fe4b70838e7835d674480346dba9ea0da4428;hb=5d4368413bdf9d8e670bab23b912994bc2f8459d;hpb=3f00169098f1cd1cdecbbf20982f7c4c58f7d71d

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index 523fe4b70..58458d1ff 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -53,3 +53,11 @@ module type Callbacks =
 val string_of_domain_item: domain_item -> string
 val string_of_domain: domain_item list -> string
 
+(** {3 type shortands} *)
+
+type term = CicAst.term
+type tactic = (term, string) TacticAst.tactic
+type tactical = (term, string) TacticAst.tactic TacticAst.tactical
+type command = term CommandAst.command
+type script = term CommandAst.Script.script
+