- 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, 4 insertions, 2 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 890f3a086..e09ba93f8 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -480,13 +480,15 @@ let _ =
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, true))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, true)))
   ]
 END
 	
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
 | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, false))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, false)))
   ]
 END