BIG FAT COMMIT REGARDING COERCIONS:

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 16f7998d19a7ee528d53f46f822b9e0a9d02a3cf..9373e54b43a1de051f743a2581220677abaf4df8 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -327,6 +327,7 @@ EXTEND
       | IDENT "solve";
         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
           GrafiteAst.Solve (loc, tacs)
+      | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
       | LPAREN; tac = SELF; RPAREN -> tac
       | tac = tactic -> GrafiteAst.Tactic (loc, tac)
       ]
@@ -385,8 +386,14 @@ EXTEND
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
-       coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; 
-       ty = term -> (name,ty,coercion) 
+       coercion = [ 
+           SYMBOL ":" -> false,0 
+         | SYMBOL ":"; SYMBOL ">" -> true,0
+         | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+       ]; 
+       ty = term -> 
+         let b,n = coercion in 
+         (name,ty,b,n) 
      ] SEP SYMBOL ";"; SYMBOL "}" -> 
       let params =
         List.fold_right
@@ -560,8 +567,9 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ->
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+        let arity = match arity with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->