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

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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index e6b1ff7e1fefc597b7b09314a60d36051c6a1e34..351d929e27e75fafb8404c9e0f62842fcb09a42b 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -30,8 +30,6 @@ exception Parse_error of string
 val parse_term:     char Stream.t -> DisambiguateTypes.term
 val parse_tactic:   char Stream.t -> DisambiguateTypes.tactic
 val parse_tactical: char Stream.t -> DisambiguateTypes.tactical
-val parse_command:  char Stream.t -> DisambiguateTypes.command
-val parse_script:   char Stream.t -> DisambiguateTypes.script
 
 (** {2 Grammar extensions} *)