X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=2d03762aecccd1bcdfa99f6be0170a97cf622070;hb=7af476a04e008ec5a7d1eaf096a4e6ce62aef6cf;hp=698539207396d537e77313dfb1c6d4df03c310f4;hpb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 698539207..2d03762ae 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -264,12 +264,9 @@ let check_l1_pattern level1_pattern level associativity =
           raise (Parse_error ("Variables can not be declared with a " ^ 
             "precedence in an associative notation"))
        (* avoid camlp5 divergence due to non-Sself recursion at the same level *)
-    | Ast.TermVar (s,Some l) when l=level -> 
-        incr variables; 
-        Ast.TermVar (s,None) 
-       (* avoid camlp5 divergence due to non-Sself left recursion *)
-    | Ast.TermVar (s,Some _) when !symbols = 0 && !variables = 0 -> 
-          raise (Parse_error "Left recursive rule with precedence not allowed")
+    | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 -> 
+          raise (Parse_error ("Left recursive rule with precedence not greater " ^
+            "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
     | Ast.TermVar _ as t -> incr variables; t
     | Ast.IdentVar _ as t -> t
     | Ast.Ascription _ -> assert false (* TODO *)
@@ -295,7 +292,7 @@ let extend (CL1P (level1_pattern,precedence)) action =
       [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
         Some (Gramext.Level level),
         [ None,
-          Some (*Gramext.NonA*) Gramext.LeftA,
+          Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, 
             (make_action
               (fun (env: CicNotationEnv.t) (loc: Ast.location) ->
@@ -355,7 +352,7 @@ let _ =
       | i when i < first -> acc
       | i ->
           aux
-            ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.LeftA, dummy_prod)
+            ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod)
              :: acc)
             (i - 1)
     in
@@ -628,7 +625,7 @@ EXTEND
     ];
   term: LEVEL "70N"
     [
-      [ p1 = term; p2 = term ->
+      [ p1 = term; p2 = term LEVEL "71N" ->
           let rec aux = function
             | Ast.Appl (hd :: tl)
             | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->