]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.mli
Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
[helm.git] / helm / software / components / content_pres / cicNotationParser.mli
index 978daf9ff99c1ce6f304663e86cb1c202f7c191a..134a42c3caf3236c20778c6ba62d64f79580610b 100644 (file)
@@ -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.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} *)