X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=26dd9b9e050ddb2707997ee69ea7cfb43978d3f0;hb=5e5d161f094982275ce39dbb4780c106e4475b37;hp=7b119ab11ac7e11db3256bb9207523ae77f6eaf0;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7b119ab11..26dd9b9e0 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -169,6 +169,8 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
+    | IDENT "applyP"; t = tactic_term ->
+        GrafiteAst.ApplyP (loc, t)
     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
@@ -657,13 +659,15 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ; 
-      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
+    | IDENT "coercion" ; 
+      t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
+      arity = OPT int ; saturations = OPT int; 
+      composites = OPT (IDENT "nocomposites") ->
         let arity = match arity with None -> 0 | Some x -> x in
         let saturations = match saturations with None -> 0 | Some x -> x in
         let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
-         (loc, UriManager.uri_of_string suri, composites, arity, saturations)
+         (loc, t, composites, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->