X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.mli;h=134a42c3caf3236c20778c6ba62d64f79580610b;hb=79d584e8f049226ec9cf68e9e06880ed0d95af51;hp=e25968bbbc4aa03cec62cda83aed3558086430e4;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli
index e25968bbb..134a42c3c 100644
--- a/helm/software/components/content_pres/cicNotationParser.mli
+++ b/helm/software/components/content_pres/cicNotationParser.mli
@@ -56,9 +56,14 @@ val level2_ast_grammar: Grammar.g
 val term : CicNotationPt.term Grammar.Entry.e
 
 val let_defs :
-  (CicNotationPt.capture_variable * CicNotationPt.term * int) list
+  (CicNotationPt.term CicNotationPt.capture_variable list * CicNotationPt.term CicNotationPt.capture_variable * CicNotationPt.term * int) list
     Grammar.Entry.e
 
+val protected_binder_vars :
+  (CicNotationPt.term list * CicNotationPt.term option) Grammar.Entry.e
+
+val parse_term: Ulexing.lexbuf -> CicNotationPt.term
+
 (** {2 Debugging} *)
 
   (** print "level2_pattern" entry on stdout, flushing afterwards *)