implemented lazy disambiguation of tactics arguments, when those

[helm.git] / helm / ocaml / cic_disambiguation / disambiguateTypes.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index 084ce012287df5d1665871fa68d0817a2a3c445a..b6d74a7fd84ff0b4b98668f5dea7a37ad079ff55 100644 (file)
--- 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