- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence

  as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
  uglily to be factorized by hand.
- Typography in RefMan-tac.tex.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 11 deletions

diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 47b36ede0..b38277cca 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -110,7 +110,7 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type hints =
+type hints_expr =
   | HintsResolve of (int option * bool * constr_expr) list
   | HintsImmediate of constr_expr list
   | HintsUnfold of reference list
@@ -124,15 +124,6 @@ type search_restriction =
   | SearchInside of reference list
   | SearchOutside of reference list
 
-type option_value =
-  | StringValue of string
-  | IntValue of int
-  | BoolValue of bool
-
-type option_ref_value =
-  | StringRefValue of string
-  | QualidRefValue of reference
-
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
@@ -144,6 +135,15 @@ type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 
+type option_value =
+  | StringValue of string
+  | IntValue of int
+  | BoolValue of bool
+
+type option_ref_value =
+  | StringRefValue of string
+  | QualidRefValue of reference
+
 type sort_expr = Rawterm.rawsort
 
 type definition_expr =
@@ -301,7 +301,7 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       rec_flag * (reference * bool * raw_tactic_expr) list
   | VernacCreateHintDb of locality_flag * lstring * bool
-  | VernacHints of locality_flag * lstring list * hints
+  | VernacHints of locality_flag * lstring list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * lreference *