notation fixed to be NON associative by default

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 698539207396d537e77313dfb1c6d4df03c310f4..2d03762aecccd1bcdfa99f6be0170a97cf622070 100644 (file)
--- 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)) ->

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 89dba29879c05208045c4685cc2e6c3f0e92b319..85edd595c2aed439e70b6e504afd0fb8bf1ee050 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -98,17 +98,16 @@ let pp_ast0 t k =
   let rec aux =
     function
     | Ast.Appl ts ->
-        let rec aux_args pos =
+        let rec aux_args level =
           function
           | [] -> []
           | [ last ] ->
-              let last = k last in
-              [ last ]
+              [ Ast.AttributedTerm (`Level level,k last) ]
           | hd :: tl ->
-              (k hd) :: aux_args `Inner tl
+              (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
         in
         add_level_info Ast.apply_prec 
-          (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
+          (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         add_level_info Ast.binder_prec
           (hvbox false true