From d97cd41db7786ee5172bb00fa2efd1c25ce44a4e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 31 Oct 2012 17:10:23 +0000
Subject: Change [Hints Resolve] to still accept constrs as arguments to
 maintain compatibility, the term is then declared as a constant internally.

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

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index f2bf542ef0..24efbcc5ef 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -91,7 +91,7 @@ GEXTEND Gram
 	  VernacHints (enforce_module_locality 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; n = OPT natural;
+      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural;
 	  dbnames = opt_hintbases ->
 	  VernacHints (use_module_locality (),dbnames,
 	    HintsResolve (List.map (fun x -> (n, true, x)) lc))
@@ -100,10 +100,14 @@ GEXTEND Gram
   obsolete_locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
+  reference_or_constr:
+   [ [ r = global -> HintsReference r
+     | "("; c = operconstr LEVEL "200"; ")" -> HintsConstr c ] ]
+  ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 global; n = OPT natural ->
+    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; n = OPT natural ->
           HintsResolve (List.map (fun x -> (n, true, x)) lc)
-      | IDENT "Immediate"; lc = LIST1 global -> HintsImmediate 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)
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
-- 
cgit v1.2.3