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
---
 intf/vernacexpr.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 97080fdad5..f1eebc18e6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -102,9 +102,13 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
+type reference_or_constr = 
+  | HintsReference of reference
+  | HintsConstr of constr_expr
+
 type hints_expr =
-  | HintsResolve of (int option * bool * reference) list
-  | HintsImmediate of reference list
+  | HintsResolve of (int option * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
   | HintsConstructors of reference list
-- 
cgit v1.2.3