]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.mli
split a term0 rule for dinamycally change top-level (i.e. non-recursive) term rul
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.mli
index 0d600cc20ef8eb93db280260904e6ae394cc6d61..a2b2251438cf91c18c1823a5c9af7d2e19b22bb0 100644 (file)
@@ -31,9 +31,15 @@ val parse_term: char Stream.t -> CicTextualParser2Ast.term
 
 (** {2 Grammar extensions} *)
 
+  (** recursive rule *)
 val term: CicTextualParser2Ast.term Grammar.Entry.e
 
-val return_term: CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> CicTextualParser2Ast.term
+  (** top level rule *)
+val term0: CicTextualParser2Ast.term Grammar.Entry.e
+
+val return_term:
+  CicTextualParser2Ast.location -> CicTextualParser2Ast.term ->
+    CicTextualParser2Ast.term
 
   (** raise a parse error *)
 val fail: CicTextualParser2Ast.location -> string -> 'a