Traduction semantique des InHyp de clause en InHypValue si local def

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

2 files changed, 16 insertions, 17 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fad326f1ab..56a5f6e46a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -506,9 +506,7 @@ let intern_inversion_strength lf ist = function
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist = function
-  | InHyp id -> InHyp (intern_hyp ist (skip_metaid id))
-  | InHypType id -> InHypType (intern_hyp ist (skip_metaid id))
+let intern_hyp_location ist (id,hl) = (intern_hyp ist (skip_metaid id), hl)
 
 (* Reads a pattern *)
 let intern_pattern evc env lfun = function
@@ -1059,9 +1057,7 @@ let interp_evaluable ist env = function
       coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))
 
 (* Interprets an hypothesis name *)
-let interp_hyp_location ist gl = function
-  | InHyp id -> InHyp (interp_hyp ist gl id)
-  | InHypType id -> InHypType (interp_hyp ist gl id)
+let interp_hyp_location ist gl (id,hl) = (interp_hyp ist gl id,hl)
 
 let eval_opt_ident ist = option_app (eval_ident ist)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 78bdd512dc..0c0a0f592e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -143,19 +143,22 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 let reduct_in_concl redfun gl = 
   convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
 
-let reduct_in_hyp redfun idref gl =
-  let inhyp,id = match idref with
-    | InHyp id -> true, id
-    | InHypType id -> false, id in
+let reduct_in_hyp redfun (id,(where,where')) gl =
   let (_,c, ty) = pf_get_hyp gl id in
-  let redfun' = under_casts (pf_reduce redfun gl) in
+  let redfun' = (*under_casts*) (pf_reduce redfun gl) in
   match c with
-    | None -> convert_hyp_no_check (id,None,redfun' ty) gl
-    | Some b ->
-	if inhyp then (* Default for defs: reduce in body *)
-	  convert_hyp_no_check (id,Some (redfun' b),ty) gl
-	else
-	  convert_hyp_no_check (id,Some b,redfun' ty) gl
+  | None -> 
+      if where = InHypValueOnly then
+	errorlabstrm "" (pr_id id ++ str "has no value");
+      if Options.do_translate () then where' := Some where;
+      convert_hyp_no_check (id,None,redfun' ty) gl
+  | Some b ->
+      let where =
+	if !Options.v7 & where = InHyp then InHypValueOnly else where in
+      let b' = if where <> InHypTypeOnly then redfun' b else b in
+      let ty' =	if where <> InHypValueOnly then redfun' ty else ty in
+      if Options.do_translate () then where' := Some where;
+      convert_hyp_no_check (id,Some b',ty') gl
 
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp   redfun id