X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.mli;h=9e3f442d87a2d66fcf2ac31713119012df33b823;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=9ed3bdefcabef9024a7b556a2ba49ce7c13c48be;hpb=78c95f6f3ed42633c4b2cbf62b816538d4208d7c;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 9ed3bdefc..9e3f442d8 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,9 +27,10 @@ exception Parse_error of Token.flocation * string (** {2 Parsing functions} *) -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_term: char Stream.t -> DisambiguateTypes.term +val parse_statement: char Stream.t -> (CicAst.term, string) TacticAst.statement +val parse_statements: + char Stream.t -> (CicAst.term, string) TacticAst.statement list (** {2 Grammar extensions} *)