X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=28d61d9e577a7ded0b59da5f7a3664736b8bc897;hb=347a92a83c3fa154c850d94b1a211fbb8334d4f1;hp=44dec6d32bf6adfc4aef459977bb26c861fe26cb;hpb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 44dec6d32..28d61d9e5 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -700,8 +700,8 @@ EXTEND
          (loc, t, composites, arity, saturations)
     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
         GrafiteAst.PreferCoercion (loc, t)
-    | IDENT "unification"; IDENT "hint"; t = tactic_term ->
-        GrafiteAst.UnificationHint (loc, t)
+    | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
+        GrafiteAst.UnificationHint (loc, t, n)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->