Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type

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

5 files changed, 50 insertions, 33 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index ffe2ff0715..81a5cfc54c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -97,15 +97,16 @@ let head_in gls indl t =
     in List.mem ity indl
   with Induc -> false
        
-let inductive_of_ident gls id =
-  match kind_of_term (pf_global gls id) with
+let inductive_of_qualid gls qid =
+  let c = Declare.construct_qualified_reference (pf_env gls) qid in
+  match kind_of_term c with
     | IsMutInd ity -> ity
     | _ ->
 	errorlabstrm "Decompose"
-	  [< pr_id id; 'sTR " is not an inductive type" >]
+	  [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >]
 
 let decompose_these c l gls =
-  let indl = List.map (inductive_of_ident gls) l in 
+  let indl = List.map (inductive_of_qualid gls) l in 
   general_decompose (fun (_,t) -> head_in gls indl t) c gls
 
 let decompose_nonrec c gls =
@@ -123,17 +124,22 @@ let decompose_or c gls =
     (fun (_,t) -> is_disjunction t)
     c gls
 
-let dyn_decompose args gl = 
+let dyn_decompose args gl =
+  let out_qualid = function
+    | Qualid qid -> qid
+    | l -> bad_tactic_args "DecomposeThese" [l] gl in
   match args with 
-    | [Clause ids; Command c] -> 
-        decompose_these (pf_interp_constr gl c) ids gl
-    | [Clause ids; Constr c]  -> 
-        decompose_these c ids  gl
+    | Command c :: ids -> 
+        decompose_these (pf_interp_constr gl c) (List.map out_qualid ids) gl
+    | Constr c :: ids  -> 
+	decompose_these c (List.map out_qualid ids) gl
     | l -> bad_tactic_args "DecomposeThese" l gl
 	  
 let h_decompose =
   let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in 
-  fun ids c -> v_decompose [Clause ids; Constr c] 
+  fun ids c ->
+    v_decompose 
+      (Constr c :: List.map (fun x -> Qualid (Nametab.qualid_of_sp x)) ids)
 
 let vernac_decompose_and = 
   hide_constr_tactic "DecomposeAnd" decompose_and
diff --git a/tactics/elim.mli b/tactics/elim.mli
index e2b9a75e35..c21d4452b9 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -29,7 +29,7 @@ val general_decompose        : (clause * constr -> bool) -> constr -> tactic
 val decompose_nonrec         : constr -> tactic
 val decompose_and            : constr -> tactic
 val decompose_or             : constr -> tactic
-val h_decompose              : identifier list -> constr -> tactic
+val h_decompose              : section_path list -> constr -> tactic
 
 val double_ind : int -> int -> tactic
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 2c4f80b748..bc07c9a4d6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -13,7 +13,7 @@ open Proof_type
 open Tacmach
 open Tacentries
 
-let h_clear ids         = v_clear  [(Clause ids)]
+let h_clear ids         = v_clear  [(Clause (List.map (fun x -> InHyp x) ids))]
 let h_move dep id1 id2  = 
  (if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
 let h_contradiction     = v_contradiction []
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d68a721f0..0e454846a0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -152,11 +152,20 @@ type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
 let reduct_in_concl redfun gl = 
   convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
     
-let reduct_in_hyp redfun id gl  = 
-  let ty = pf_get_hyp_typ gl id in
+let reduct_in_hyp redfun idref gl =
+  let inhyp,id = match idref with
+    | InHyp id -> true, id
+    | InHypType id -> false, id in
+  let c, ty = pf_get_hyp gl id in
   let redfun' = under_casts (pf_reduce redfun gl) in
-  convert_hyp id (redfun' ty) gl
-    
+  match c with
+    | None -> convert_hyp id (redfun' ty) gl
+    | Some b ->
+	if inhyp then (* Default for defs: reduce in body *)
+	  convert_defbody id (redfun' b) gl
+	else
+	  convert_deftype id (redfun' ty) gl
+
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp   redfun id 
   | None    -> reduct_in_concl redfun 
@@ -783,7 +792,9 @@ let dyn_assumption = function
 let clear ids gl    = thin ids gl
 let clear_one id gl = clear [id] gl
 let dyn_clear = function
-  | [Clause ids] -> clear ids
+  | [Clause ids] ->
+      let out = function InHyp id -> id | _ -> assert false in
+      clear (List.map out ids)
   | _ -> assert false
 
 (* Clears a list of identifiers clauses form the context *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 07db3b4590..6f315f358b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,39 +102,39 @@ val dyn_exact_check  : tactic_arg list -> tactic
 
 type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
 
-val reduct_in_hyp     : 'a tactic_reduction -> identifier -> tactic
-val reduct_option     : 'a tactic_reduction -> identifier option -> tactic
+val reduct_in_hyp     : 'a tactic_reduction -> hyp_location -> tactic
+val reduct_option     : 'a tactic_reduction -> hyp_location option -> tactic
 val reduct_in_concl   : 'a tactic_reduction -> tactic
 val change_in_concl   : constr -> tactic
 
-val change_in_hyp     : constr -> identifier -> tactic
-val change_option     : constr -> identifier option -> tactic
+val change_in_hyp     : constr -> hyp_location -> tactic
+val change_option     : constr -> hyp_location option -> tactic
 val red_in_concl      : tactic
-val red_in_hyp        : identifier        -> tactic
-val red_option        : identifier option -> tactic
+val red_in_hyp        : hyp_location        -> tactic
+val red_option        : hyp_location option -> tactic
 val hnf_in_concl      : tactic
-val hnf_in_hyp        : identifier        -> tactic
-val hnf_option        : identifier option -> tactic
+val hnf_in_hyp        : hyp_location        -> tactic
+val hnf_option        : hyp_location option -> tactic
 val simpl_in_concl    : tactic
-val simpl_in_hyp      : identifier        -> tactic
-val simpl_option      : identifier option -> tactic
+val simpl_in_hyp      : hyp_location        -> tactic
+val simpl_option      : hyp_location option -> tactic
 val normalise_in_concl: tactic
-val normalise_in_hyp  : identifier        -> tactic
-val normalise_option  : identifier option -> tactic
+val normalise_in_hyp  : hyp_location        -> tactic
+val normalise_option  : hyp_location option -> tactic
 val unfold_in_concl   : (int list * Closure.evaluable_global_reference) list
   -> tactic
 val unfold_in_hyp     : 
-  (int list * Closure.evaluable_global_reference) list -> identifier -> tactic
+  (int list * Closure.evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (int list * Closure.evaluable_global_reference) list -> identifier option
+  (int list * Closure.evaluable_global_reference) list -> hyp_location option
     -> tactic
-val reduce            : red_expr -> identifier list -> tactic
+val reduce            : red_expr -> hyp_location list -> tactic
 val dyn_reduce        : tactic_arg list -> tactic
 val dyn_change        : tactic_arg list -> tactic
 
 val unfold_constr     : global_reference -> tactic
 val pattern_option    : 
-  (int list * constr * constr) list -> identifier option -> tactic
+  (int list * constr * constr) list -> hyp_location option -> tactic
 
 (*s Modification of the local context. *)