X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateTypes.mli;h=b6d74a7fd84ff0b4b98668f5dea7a37ad079ff55;hb=d1126c6b78a3333bbf415daf027004496b77c2f4;hp=084ce012287df5d1665871fa68d0817a2a3c445a;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index 084ce0122..b6d74a7fd 100644
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -70,8 +70,8 @@ val string_of_domain: domain_item list -> string
 (** {3 type shortands} *)
 
 type term = CicNotationPt.term
-type tactic = (term, string) GrafiteAst.tactic
-type tactical = (term, string) GrafiteAst.tactical
+type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic
+type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical
 
 type script_entry =
   | Command of tactical