X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.mli;h=433711edd29ab9c5620641ace4704fa073b0c352;hb=279b11c00cdaacb4858e1c8dc6d05ea631bc1358;hp=6c9b3f5ecfa46ae8be23a55b6fad5ecc0cdb13dd;hpb=eb9ca860db8cb06083765f7698179f16dee5303e;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index 6c9b3f5ec..433711edd 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -57,15 +57,15 @@ val delete: rule_id -> unit (** {2 Grammar entries} * needed by grafite parser *) -val level2_ast_grammar: Grammar.g +val level2_ast_grammar: unit -> Grammar.g -val term : CicNotationPt.term Grammar.Entry.e +val term : unit -> CicNotationPt.term Grammar.Entry.e -val let_defs : +val let_defs : unit -> (CicNotationPt.term CicNotationPt.capture_variable list * CicNotationPt.term CicNotationPt.capture_variable * CicNotationPt.term * int) list Grammar.Entry.e -val protected_binder_vars : +val protected_binder_vars : unit -> (CicNotationPt.term list * CicNotationPt.term option) Grammar.Entry.e val parse_term: Ulexing.lexbuf -> CicNotationPt.term