X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguateTypes.ml;h=6c530c2bf4813d16bb06da7eb882d4562f0f04ac;hb=3a12950125e7a4a792546aacea40505f3cecae89;hp=c30316769b5cb1ad94dce5a26bc899c197120d8f;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index c30316769..6c530c2bf 100644
--- 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