X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=9f5fd193e9d170c05ef4fe9473e175c9805d251d;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=add74d03e856cde6162bf7064d66f3ec6da489c9;hpb=a4c955f9b69cae88879d366b01ac86fa1ea2b829;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index add74d03e..9f5fd193e 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec"
 let macro = Grammar.Entry.create grammar "macro"
 let script = Grammar.Entry.create grammar "script"
 let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 
@@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body =
     vars body
 
 EXTEND
-  GLOBAL: term term0 statement;
+  GLOBAL: term term0 statement statements;
   int: [
     [ num = NUM ->
         try
@@ -147,20 +148,18 @@ EXTEND
     ]
   ];
   subst: [
-    [ subst = OPT [
-        SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
-        PAREN "[";
-        substs = LIST1 [
-          i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
-        ] SEP SYMBOL ";";
-        PAREN "]" ->
-          substs
-      ] -> subst
+    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+      PAREN "[";
+      substs = LIST1 [
+        i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
+      ] SEP SYMBOL ";";
+      PAREN "]" ->
+        substs
     ]
   ];
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
-    [ s = IDENT; subst = subst -> CicAst.Ident (s, subst)
-    | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst)
+    [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst)
+    | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst)
     ]
   ];
   name: [ (* as substituted_name with no explicit substitution *)
@@ -588,6 +587,10 @@ EXTEND
     | com = comment -> TacticAst.Comment (loc, com)
     ]
   ];
+  statements: [
+    [ l = LIST0 [ statement ] -> l 
+    ]  
+  ];
 END
 
 let exc_located_wrapper f =
@@ -603,6 +606,9 @@ let parse_term stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+  
 
 (**/**)