Filled pre-generated notation levels with productions on dummy tokens (never generate...

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 13817e248e08b013c31c212cb92a5fdb8478f24d..90324541da82ba83f4e47d0188f886188e292e68 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -278,15 +278,23 @@ let fold_binder binder pt_names body =
 
 let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
 
-let _ = (* create empty precedence level for "term" *)
+  (* create empty precedence level for "term" *)
+let _ =
+  let dummy_action =
+    Gramext.action (fun _ ->
+      failwith "internal error, lexer generated a dummy token")
+  in
+  (* Needed since campl4 on "delete_rule" remove the precedence level if it gets
+   * empty after the deletion. The lexer never generate the Stoken below. *)
+  let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
   let mk_level_list first last =
     let rec aux acc = function
       | i when i < first -> acc
       | i ->
           aux
-            ((Some (string_of_int i ^ "N"), Some Gramext.NonA, [])
-             :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, [])
-             :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, [])
+            ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod)
+             :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod)
+             :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod)
              :: acc)
             (i - 1)
     in