- partial implementation of pattern for case documented

[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 6fcb9dba4f0a8e83620b84534f68523ef2d1cd07..18c30d4ecbddcfa141c229131223d6c8149f3761 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -55,7 +55,6 @@ let statement = Grammar.Entry.create grammar "statement"
 
 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
-let default_precedence = 50
 let default_associativity = Gramext.NonA
         
 let mk_rec_corec ind_kind defs loc = 
@@ -177,8 +176,13 @@ EXTEND
     | IDENT "autobatch";  params = auto_params ->
         GrafiteAst.AutoBatch (loc,params)
     | IDENT "cases"; what = tactic_term;
+      pattern = OPT pattern_spec;
       specs = intros_spec ->
-        GrafiteAst.Cases (loc, what, specs)
+        let pattern = match pattern with
+           | None         -> None, [], Some Ast.UserInput
+           | Some pattern -> pattern   
+        in
+        GrafiteAst.Cases (loc, what, pattern, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
@@ -570,7 +574,7 @@ EXTEND
   ];
   notation: [
     [ dir = OPT direction; s = QSTRING;
-      assoc = OPT associativity; prec = OPT precedence;
+      assoc = OPT associativity; prec = precedence;
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
@@ -587,11 +591,6 @@ EXTEND
             | None -> default_associativity
             | Some assoc -> assoc
           in
-          let prec =
-            match prec with
-            | None -> default_precedence
-            | Some prec -> prec
-          in
           let p1 =
             add_raw_attribute ~text:s
               (CicNotationParser.parse_level1_pattern