new dependences

[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 44dec6d32bf6adfc4aef459977bb26c861fe26cb..28d61d9e577a7ded0b59da5f7a3664736b8bc897 100644 (file)
--- 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 ->