3 files changed, 45 insertions, 13 deletions
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index d1ac0862ed..a012f1cb15 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -32,31 +32,29 @@ type head_approximation =
 | FlexibleHead of int * int * int * bool (* [true] if a surrounding case *)
 | NotImmediatelyComputableHead
 
-(* FIXME: maybe change interface here *)
-let rec compute_head env = function
-  | EvalConstRef cst ->
-    let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in
-    (match body with
-     | None -> RigidHead (RigidParameter cst)
-     | Some c -> kind_of_head env c)
-  | EvalVarRef id ->
-    (match lookup_named id env with
-     | LocalDef (_,c,_) -> kind_of_head env c
-     | _ -> RigidHead RigidOther)
+let rec compute_head_const env cst =
+  let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in
+  match body with
+  | None -> RigidHead (RigidParameter cst)
+  | Some c -> kind_of_head env c
+
+and compute_head_var env id = match lookup_named id env with
+| LocalDef (_,c,_) -> kind_of_head env c
+| _ -> RigidHead RigidOther
 
 and kind_of_head env t =
   let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
-      (try on_subterm k l b (compute_head env (EvalVarRef id))
+      (try on_subterm k l b (compute_head_var env id)
        with Not_found ->
         (* a goal variable *)
         match lookup_named id env with
         | LocalDef (_,c,_) -> aux k l c b
         | LocalAssum _ -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
-      (try on_subterm k l b (compute_head env (EvalConstRef cst))
+      (try on_subterm k l b (compute_head_const env cst)
        with Not_found ->
          CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c705ac16e7..411fb0cd89 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -43,6 +43,25 @@ exception ReductionTacticError of reduction_tactic_error
 exception Elimconst
 exception Redelimination
 
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+(* Better to have it here that in closure, since used in grammar.cma *)
+let eq_egr e1 e2 = match e1, e2 with
+    EvalConstRef con1, EvalConstRef con2 -> Constant.CanOrd.equal con1 con2
+  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
+  | _, _ -> false
+
+(* Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
+let subst_evaluable_reference subst = function
+  | EvalVarRef id -> EvalVarRef id
+  | EvalConstRef kn -> EvalConstRef (Mod_subst.subst_constant subst kn)
+
 let error_not_evaluable r =
   user_err ~hdr:"error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 65e3421736..aa232175bb 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -18,6 +18,21 @@ open Locus
 open Univ
 open Ltac_pretype
 
+(* XXX: Move to a module *)
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
+
+(** Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
+val subst_evaluable_reference :
+  Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_reference
+
 type reduction_tactic_error =
     InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)