missing file added

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 20aad1cd3a19c16788264e634cb95028cca31c89..7b119ab11ac7e11db3256bb9207523ae77f6eaf0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -95,7 +95,7 @@ type by_continuation =
 EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
-  tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
+  tactic_term: [ [ t = term LEVEL "90" -> t ] ];
   new_name: [
     [ id = IDENT -> Some id
     | SYMBOL "_" -> None ]
@@ -593,7 +593,7 @@ EXTEND
           in
           let p1 =
             add_raw_attribute ~text:s
-              (CicNotationParser.parse_level1_pattern
+              (CicNotationParser.parse_level1_pattern prec
                 (Ulexing.from_utf8_string s))
           in
           (dir, p1, assoc, prec, p2)