- 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, 34 insertions, 10 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 55df4b185e..34187c919b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -35,15 +35,20 @@ exception ReductionTacticError of reduction_tactic_error
 exception Elimconst
 exception Redelimination
 
+let error_not_evaluable r =
+  errorlabstrm "error_not_evaluable"
+    (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Idset.empty r ++ 
+     spc () ++ str "to an evaluable reference.")
+
+let is_evaluable_const env cst =
+  is_transparent (ConstKey cst) && evaluable_constant cst env
+
+let is_evaluable_var env id =
+  is_transparent (VarKey id) && evaluable_named id env
+
 let is_evaluable env = function
-  | EvalConstRef kn ->
-      is_transparent (ConstKey kn) &&
-      let cb = Environ.lookup_constant kn env in
-      cb.const_body <> None & not cb.const_opaque
-  | EvalVarRef id ->
-      is_transparent (VarKey id) &&
-      let (_,value,_) = Environ.lookup_named id env in
-      value <> None
+  | EvalConstRef cst -> is_evaluable_const env cst
+  | EvalVarRef id -> is_evaluable_var env id
 
 let value_of_evaluable_ref env = function
   | EvalConstRef con -> constant_value env con
@@ -53,6 +58,15 @@ let constr_of_evaluable_ref = function
   | EvalConstRef con -> mkConst con
   | EvalVarRef id -> mkVar id
 
+let evaluable_of_global_reference env = function
+  | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
+  | VarRef id when is_evaluable_var env id -> EvalVarRef id
+  | r -> error_not_evaluable r
+
+let global_of_evaluable_reference = function
+  | EvalConstRef cst -> ConstRef cst
+  | EvalVarRef id -> VarRef id
+
 type evaluable_reference =
   | EvalConst of constant
   | EvalVar of identifier
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 1516a2bd6a..c29a3f335a 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -26,7 +26,17 @@ exception ReductionTacticError of reduction_tactic_error
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
 
-val is_evaluable : env -> evaluable_global_reference -> bool
+(* Evaluable global reference *)
+
+val is_evaluable : Environ.env -> evaluable_global_reference -> bool
+
+val error_not_evaluable : Libnames.global_reference -> 'a
+
+val evaluable_of_global_reference :
+  Environ.env -> Libnames.global_reference -> evaluable_global_reference
+
+val global_of_evaluable_reference :
+  evaluable_global_reference -> Libnames.global_reference
 
 exception Redelimination
 
@@ -75,7 +85,7 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
 (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
-   [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *)
+   [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types