- 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

2 files changed, 12 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 1014a6545c..82b1afabfb 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -49,6 +49,12 @@ exception Error_in_file of string * (bool * string * loc) * exn
 let on_fst f (a,b) = (f a,b)
 let on_snd f (a,b) = (a,f b)
 
+(* Mapping under pairs *)
+
+let on_pi1 f (a,b,c) = (f a,b,c)
+let on_pi2 f (a,b,c) = (a,f b,c)
+let on_pi3 f (a,b,c) = (a,b,f c)
+
 (* Projections from triplets *)
 
 let pi1 (a,_,_) = a
diff --git a/lib/util.mli b/lib/util.mli
index 0acff599db..04d3a52fcf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -59,6 +59,12 @@ exception Error_in_file of string * (bool * string * loc) * exn
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 
+(* Mapping under triple *)
+
+val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
+val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd
+val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b
+
 (*s Projections from triplets *)
 
 val pi1 : 'a * 'b * 'c -> 'a