implemented lazy disambiguation of tactics arguments, when those

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index c30316769b5cb1ad94dce5a26bc899c197120d8f..6c530c2bf4813d16bb06da7eb882d4562f0f04ac 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -24,8 +24,8 @@
  *)
 
 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
   | Comment of CicNotationPt.location * string