- moved command as sub-entries of tactical grammars (as per tactics)

[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 358f2d49ec99ea62d790bd0b74daa076b0d891ef..a5e0f96f838b48b1e04cacc3aa2cae96ad11d8f8 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -25,9 +25,7 @@
 
 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
+type tactical = (term, string) TacticAst.tactical
 
 type domain_item =
  | Id of string               (* literal *)