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

9 files changed, 49 insertions, 32 deletions

diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index b047e01f1..ec4282fa2 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -211,4 +211,4 @@ let normalize_evaluables=
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some id-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (Tacexpr.InHypType id))
+	   (id,(Tacexpr.InHypTypeOnly,ref None)))
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 74352c0bb..491fd467f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -217,8 +217,9 @@ GEXTEND Gram
       | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
   ;
   hypident:
-    [ [ id = id_or_meta -> InHyp id
-      | "("; "Type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
+    [ [ id = id_or_meta -> id,(InHyp,ref None)
+      | "("; "Type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
+    ] ]
   ;
   clause:
     [ [ "in"; idl = LIST1 hypident -> idl
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 45253cd90..29dc5cfba 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -268,8 +268,10 @@ GEXTEND Gram
       | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
   ;
   hypident:
-    [ [ id = id_or_meta -> InHyp id
-      | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
+    [ [ id = id_or_meta -> id,(InHyp,ref None)
+      | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
+      | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None)
+    ] ]
   ;
   clause:
     [ [ "in"; idl = LIST1 hypident -> idl
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8f0a29c64..ea5ad236e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -136,8 +136,9 @@ let pr_with_names = function
   | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
 
 let pr_hyp_location pr_id = function
-  | InHyp id -> spc () ++ pr_id id
-  | InHypType id -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
+  | id, (InHyp,_) -> spc () ++ pr_id id
+  | id, (InHypTypeOnly,_) -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
+  | id, _ -> error "Unsupported hyp location in v7"
 
 let pr_clause pr_id = function
   | [] -> mt ()
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 7dd14d87a..01be09fc6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -159,8 +159,9 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >>
 let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
 
 let mlexpr_of_hyp_location = function
-  | Tacexpr.InHyp id -> <:expr< Tacexpr.InHyp $mlexpr_of_hyp id$ >>
-  | Tacexpr.InHypType id -> <:expr< Tacexpr.InHypType $mlexpr_of_hyp id$ >>
+  | id, (Tacexpr.InHyp,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHyp, ref None)) >>
+  | id, (Tacexpr.InHypTypeOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypTypeOnly, ref None)) >>
+  | id, (Tacexpr.InHypValueOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypValueOnly,ref None)) >>
 
 (*
 let mlexpr_of_red_mode = function
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 7ded6b4c9..5de120dbb 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -50,9 +50,13 @@ let make_red_flag =
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
 
-type 'a raw_hyp_location = (* To distinguish body and type of local defs *)
-  | InHyp of 'a
-  | InHypType of 'a
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+type 'a raw_hyp_location = 
+    'a * (hyp_location_flag * hyp_location_flag option ref)
 
 type 'a induction_arg =
   | ElimOnConstr of 'a
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fad326f1a..56a5f6e46 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 78bdd512d..0c0a0f592 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 
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a7181e13b..565da88ca 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -206,12 +206,21 @@ let pr_with_names = function
   | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
 
 let pr_hyp_location pr_id = function
-  | InHyp id -> spc () ++ pr_id id
-  | InHypType id -> spc () ++ str "(type of " ++ pr_id id ++ str ")"
+  | id, InHyp -> spc () ++ pr_id id
+  | id, InHypTypeOnly -> spc () ++ str "(type of " ++ pr_id id ++ str ")"
+  | id, InHypValueOnly -> spc () ++ str "(value of " ++ pr_id id ++ str ")"
+
+let pr_hyp_location pr_id (id,(hl,hl')) =
+  if !hl' <> None then pr_hyp_location pr_id (id,out_some !hl')
+  else
+    (if hl = InHyp && Options.do_translate () then 
+      msgerrnl (str "Warning: Unable to detect if " ++ pr_id id ++ str " denots a local definition; if it is the case, the translation is wrong");
+    pr_hyp_location pr_id (id,hl))
 
 let pr_clause pr_id = function
   | [] -> mt ()
-  | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
+  | l ->
+      spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
 
 let pr_simple_clause pr_id = function
   | [] -> mt ()