X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.mli;h=c95485e52661b20b1028c53d8eddf42cb672c967;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;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..c95485e52 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,9 +27,11 @@ 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, TacticAst.obj,string) TacticAst.statement +val parse_statements: + char Stream.t -> (CicAst.term, TacticAst.obj, string) TacticAst.statement list (** {2 Grammar extensions} *)