From ea37ffa0d9c1bf2e18f843fd2fddba32b7b04de8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 7 Sep 2013 09:19:44 +0000
Subject: Change syntax of Hint Resolve to actually accept user-given
 priorities.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16766 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofs.ml4 | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 3090fd7f32..e2be4b6071 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -91,10 +91,11 @@ GEXTEND Gram
 	  VernacHints (local,dbnames, h)
       (* Declare "Resolve" explicitly so as to be able to later extend with
          "Resolve ->" and "Resolve <-" *)
-      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural;
+      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
+	  pri = OPT [ "|"; i = natural -> i ];
 	  dbnames = opt_hintbases ->
 	  VernacHints (false,dbnames,
-	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
+	    HintsResolve (List.map (fun x -> (pri, true, x)) lc))
       ] ];
 
   obsolete_locality:
@@ -105,8 +106,9 @@ GEXTEND Gram
      | c = constr -> HintsConstr c ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural ->
-          HintsResolve (List.map (fun x -> (n, true, x)) lc)
+    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; 
+	pri = OPT [ "|"; i = natural -> i ] ->
+          HintsResolve (List.map (fun x -> (pri, true, x)) lc)
       | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
       | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
-- 
cgit v1.2.3