X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.mli;h=53182dc3167d6d8ae8e119b444561d7137a0547a;hb=14724f9aab44f1b150a5509743a43cb6693d493e;hp=978daf9ff99c1ce6f304663e86cb1c202f7c191a;hpb=774c8d18f41e71ae7e26a90d726d10a6f95de1fe;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli
index 978daf9ff..53182dc31 100644
--- a/helm/software/components/content_pres/cicNotationParser.mli
+++ b/helm/software/components/content_pres/cicNotationParser.mli
@@ -56,9 +56,12 @@ val level2_ast_grammar: Grammar.g
 val term : CicNotationPt.term Grammar.Entry.e
 
 val let_defs :
-  (CicNotationPt.capture_variable * CicNotationPt.term * int) list
+  (CicNotationPt.capture_variable list * 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} *)