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

18 files changed, 204 insertions, 75 deletions

diff --git a/.depend b/.depend
index d7c1472ced..5e7ab5e0e8 100644
--- a/.depend
+++ b/.depend
@@ -983,16 +983,16 @@ tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
-tactics/elim.cmo: proofs/clenv.cmi tactics/hiddentac.cmi \
-    tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
-    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
-    tactics/elim.cmi 
-tactics/elim.cmx: proofs/clenv.cmx tactics/hiddentac.cmx \
-    tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx proofs/tacmach.cmx \
-    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
-    tactics/elim.cmi 
+tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi tactics/hiddentac.cmi \
+    tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi tactics/elim.cmi 
+tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx tactics/hiddentac.cmx \
+    tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx tactics/elim.cmi 
 tactics/eqdecide.cmo: tactics/auto.cmi parsing/coqlib.cmi \
     tactics/equality.cmi library/global.cmi tactics/hiddentac.cmi \
     tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
@@ -1127,6 +1127,12 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \
     kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
     proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
     kernel/term.cmx lib/util.cmx tactics/tactics.cmi 
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+    kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi 
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+    kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx 
 tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi pretyping/pattern.cmi \
     pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi 
 tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx pretyping/pattern.cmx \
diff --git a/.depend.camlp4 b/.depend.camlp4
index 6612744a1c..ac3ad8320d 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,4 +1,4 @@
-tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
+tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 contrib/correctness/psyntax.ml: parsing/grammar.cma
 contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 parsing/lexer.ml: 
diff --git a/CHANGES b/CHANGES
index 3b1e5bd1eb..a909449f67 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,13 @@
+Modifications depuis la V7.0
+
+- Fonctions de réduction dans les définitions locales s'appliquent par
+  défaut au corps de la définition. Extension de la notion de Clause
+  pour forcer l'action sur le type des défs seulement sous la forme
+  "Change c in Type of H."
+- Prise en compte des qualid dans Decompose
+- Correction bug inférence type Cases en présence de K-rédex
+- Correction bugs Cases en cas de prédicat dépendant
+
 Différences V7.0beta / V7.0
 - Portage de Correctness
 - Réécriture de Extraction
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 70aaba18d1..c374f59557 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -54,6 +54,9 @@ GEXTEND Gram
     [ [ id = Constr.ident -> id
       | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> ] ]
   ;
+  idmetahyp:
+    [ [ id = idmeta_arg -> <:ast< (INHYP $id) >> ] ]
+  ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
       | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ]
@@ -94,8 +97,8 @@ GEXTEND Gram
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
-  ne_idmeta_arg_list:
-    [ [ l = LIST1 idmeta_arg -> l ] ]
+  ne_idmetahyp_list:
+    [ [ l = LIST1 idmetahyp -> l ] ]
   ;
   ne_qualidarg_list:
     [ [ l = LIST1 qualidarg -> l ] ]
@@ -211,8 +214,15 @@ GEXTEND Gram
       | IDENT "Pattern"; pl = ne_pattern_list ->
           <:ast< (Pattern ($LIST $pl)) >> ] ]
   ;
+  hypident:
+    [ [ id = identarg -> <:ast< (INHYP $id) >>
+      | "("; "Type"; "of"; id = identarg; ")" -> <:ast< (INHYPTYPE $id) >> ] ]
+  ;
+  ne_hyp_list:
+    [ [ l = LIST1 hypident -> l ] ]
+  ;
   clausearg:
-    [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
+    [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST idl)) >>
       | -> <:ast< (CLAUSE) >> ] ]
   ;
   fixdecl:
@@ -225,9 +235,6 @@ GEXTEND Gram
           <:ast< (COFIXEXP $id $c) >> :: fd
       | -> [] ] ]
   ;
- END
-
-GEXTEND Gram
   simple_tactic:
     [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
       | IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >>
@@ -300,8 +307,8 @@ GEXTEND Gram
              <:ast< (DecomposeAnd $c) >>
       | IDENT "Decompose"; IDENT "Sum"; c = constrarg -> 
              <:ast< (DecomposeOr $c) >>
-      | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
-          <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
+      | IDENT "Decompose"; "["; l = ne_qualidarg_list; "]"; c = constrarg ->
+          <:ast< (DecomposeThese $c ($LIST $l)) >>
       | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
       | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
@@ -314,7 +321,7 @@ GEXTEND Gram
       | IDENT "LetTac"; s = identarg; ":="; c = constrarg; p = clause_pattern->
 	  <:ast< (LetTac $s $c $p) >>
       | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
-      | IDENT "Clear"; l = ne_idmeta_arg_list -> 
+      | IDENT "Clear"; l = ne_idmetahyp_list -> 
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ff103ae2ca..849d2639cc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -292,7 +292,9 @@ module Tactic =
     let constrarg_list = gec_list "constrarg_list"
     let ident_or_constrarg = gec "ident_or_constrarg"
     let identarg = gec "identarg"
+    let hypident = gec "hypident"
     let idmeta_arg = gec "idmeta_arg"
+    let idmetahyp = gec "idmetahyp"
     let qualidarg = gec "qualidarg"
     let qualidconstarg = gec "qualidconstarg"
     let input_fun = gec "input_fun"
@@ -307,7 +309,8 @@ module Tactic =
     let match_rule = gec "match_rule"
     let match_list = gec_list "match_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
-    let ne_idmeta_arg_list = gec_list "ne_idmeta_arg_list"
+    let ne_hyp_list = gec_list "ne_hyp_list"
+    let ne_idmetahyp_list = gec_list "ne_idmetahyp_list"
     let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 30773eaa6a..b9c77509e2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -116,7 +116,9 @@ module Tactic :
     val fixdecl : Coqast.t list Gram.Entry.e
     val ident_or_constrarg : Coqast.t Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
+    val hypident : Coqast.t Gram.Entry.e
     val idmeta_arg : Coqast.t Gram.Entry.e
+    val idmetahyp : Coqast.t Gram.Entry.e
     val qualidarg : Coqast.t Gram.Entry.e
     val qualidconstarg : Coqast.t Gram.Entry.e
     val input_fun : Coqast.t Gram.Entry.e
@@ -132,7 +134,8 @@ module Tactic :
     val match_rule : Coqast.t Gram.Entry.e
     val match_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
-    val ne_idmeta_arg_list : Coqast.t list Gram.Entry.e
+    val ne_hyp_list : Coqast.t list Gram.Entry.e
+    val ne_idmetahyp_list : Coqast.t list Gram.Entry.e
     val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3f22a6f8ba..a5fe2d5962 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -266,13 +266,37 @@ let check_forward_dependencies id tail =
 		^ (string_of_id id')))
     tail
 
-let convert_hyp sign sigma id ty =
+let convert_hyp sign sigma id b =
   apply_to_hyp sign id
     (fun sign (idc,c,ct) _ ->
        let env = Global.env_of_context sign in
-       if !check && not (is_conv env sigma ty (body_of_type ct)) then
-	 error "convert-hyp rule passed non-converting term";
-       add_named_decl (idc,c,ty) sign)
+       match c with
+	 | None -> (* Change the type *)
+	     if !check && not (is_conv env sigma b ct) then
+	       error "convert-hyp rule passed non-converting term";
+	     add_named_decl (idc,c,b) sign
+	 | Some c -> (* Change the body *)
+	     if !check && not (is_conv env sigma b c) then
+	       error "convert-hyp rule passed non-converting term";
+	     add_named_decl (idc,Some b,ct) sign)
+
+let convert_def inbody sign sigma id c =
+  apply_to_hyp sign id
+    (fun sign (idc,b,t) _ ->
+       let env = Global.env_of_context sign in
+       match b with
+	 | None -> error "convert-deftype rule passed to an hyp without body" 
+	 | Some b ->
+	     let b,t = 
+	       if inbody then
+		 (if !check && not (is_conv env sigma c b) then 
+		    error "convert-deftype rule passed non-converting type";
+		  (c,t))
+	       else
+		 (if !check && not (is_conv env sigma c t) then
+		    error "convert-deftype rule passed non-converting type";
+		  (b,c)) in
+	     add_named_decl (idc,Some b,t) sign)
 
 let replace_hyp sign id d =
   apply_to_hyp sign id
@@ -445,8 +469,14 @@ let prim_refiner r sigma goal =
 	else 
 	  error "convert-concl rule passed non-converting term"
 
-    | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } ->
-	[mk_goal info (convert_hyp sign sigma id ty') cl]
+    | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
+	[mk_goal info (convert_hyp sign sigma id ty) cl]
+
+    | { name = Convert_defbody; hypspecs = [id]; terms = [c] } ->
+	[mk_goal info (convert_def true sign sigma id c) cl]
+
+    | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
+	[mk_goal info (convert_def false sign sigma id ty) cl]
 
     | { name = Thin; hypspecs = ids } ->
 	let clear_aux sign id =
@@ -537,7 +567,13 @@ let prim_extractor subfun vl pft =
     | {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} ->
 	subfun vl pf
 	
-    | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[c]},[pf])} ->
+    | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[_]},[pf])} ->
+	subfun vl pf
+
+    | {ref=Some(Prim{name=Convert_defbody;hypspecs=[id];terms=[_]},[pf])} ->
+	subfun vl pf
+
+    | {ref=Some(Prim{name=Convert_deftype;hypspecs=[id];terms=[_]},[pf])} ->
 	subfun vl pf
 	
     | {ref=Some(Prim{name=Thin;hypspecs=ids},[pf])} ->
@@ -600,6 +636,13 @@ let pr_prim_rule = function
   | {name=Convert_hyp;hypspecs=[id];terms=[c]} ->
       [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
       
+  | {name=Convert_defbody;hypspecs=[id];terms=[c]} ->
+      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
+
+  | {name=Convert_deftype;hypspecs=[id];terms=[c]} ->
+      [< 'sTR"Change " ; prterm c ; 'sPC ;
+	 'sTR"in (Type of " ; pr_id id; 'sTR ")" >]
+      
   | {name=Thin;hypspecs=ids} ->
       [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >]
       
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 18cd475cde..45fe9e5a47 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -407,7 +407,11 @@ let ast_of_cvt_arg = function
   | Constr_context _ ->
     anomalylabstrm "ast_of_cvt_arg" [<'sTR
       "Constr_context argument could not be used">]
-  | Clause idl      -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
+  | Clause idl      -> 
+      let transl = function
+	| InHyp id -> ope ("INHYP", [nvar (string_of_id id)])
+	| InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in
+      ope ("CLAUSE", List.map transl idl)
   | Bindings bl     -> ope ("BINDINGS", 
 			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
   | Cbindings bl    -> 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index bf8deb53a5..363dd09645 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -28,6 +28,10 @@ type pf_status =
   | Complete_proof
   | Incomplete_proof
 
+type hyp_location = (* To distinguish body and type of local defs *)
+  | InHyp of identifier
+  | InHypType of identifier
+
 type prim_rule_name = 
   | Intro
   | Intro_after
@@ -37,6 +41,8 @@ type prim_rule_name =
   | Refine 
   | Convert_concl
   | Convert_hyp
+  | Convert_defbody
+  | Convert_deftype
   | Thin
   | Move of bool
 
@@ -97,7 +103,7 @@ and tactic_arg =
   | Identifier     of identifier
   | Qualid         of Nametab.qualid
   | Integer        of int
-  | Clause         of identifier list
+  | Clause         of hyp_location list
   | Bindings       of Coqast.t substitution
   | Cbindings      of constr   substitution 
   | Quoted_string  of string
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index de2c155f07..5d415d5a08 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -31,6 +31,10 @@ type pf_status =
   | Complete_proof
   | Incomplete_proof
 
+type hyp_location = (* To distinguish body and type of local defs *)
+  | InHyp of identifier
+  | InHypType of identifier
+
 type prim_rule_name = 
   | Intro
   | Intro_after
@@ -40,6 +44,8 @@ type prim_rule_name =
   | Refine 
   | Convert_concl
   | Convert_hyp
+  | Convert_defbody
+  | Convert_deftype
   | Thin
   | Move of bool
 
@@ -129,7 +135,7 @@ and tactic_arg =
   | Identifier     of identifier
   | Qualid         of Nametab.qualid
   | Integer        of int
-  | Clause         of identifier list
+  | Clause         of hyp_location list
   | Bindings       of Coqast.t substitution
   | Cbindings      of constr   substitution 
   | Quoted_string  of string
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 4b45132455..35435f7a70 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -529,6 +529,10 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
        | Invalid_argument "destVar" ->
          user_err_loc (loc, "Tacinterp.val_interp",[<'sTR
           "Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))*)
+    | Node(loc,"QUALIDARG",p) -> VArg (Qualid (interp_qualid p))
+    | Node(loc,"QUALIDMETA",[Num(_,n)]) ->
+	VArg
+	  (Qualid (Nametab.qualid_of_sp (path_of_const (List.assoc n lmatch))))
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
     | Node(_,"COMMAND",[c]) ->
@@ -544,8 +548,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug)
         (redname,args)))
     | Node(_,"CLAUSE",cl) ->
-      VArg (Clause (List.map (fun ast -> make_ids ast (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt,debug) ast))) cl))
+      VArg (Clause (List.map (clause_interp 
+        (evc,env,lfun,lmatch,goalopt,debug)) cl))
     | Node(_,"TACTIC",[ast]) ->
       VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
 (*Remains to treat*)
@@ -1170,7 +1174,14 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function
       error "\"Goal\" occurs twice"
     else
       (Some (List.map num_of_ast nums), l)
-  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern")
+  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_letpattern")
+
+(* Interprets an hypothesis name *)
+and clause_interp info = function
+  | Node(_,("INHYP"|"INHYPTYPE" as where),[ast]) ->
+      let id = make_ids ast (unvarg (val_interp info ast)) in
+      if where = "INHYP" then InHyp id else InHypType id
+  | arg -> invalid_arg_loc (Ast.loc arg,"clause_interp")
 
 (* Interprets tactic arguments *)
 let interp_tacarg sign ast = unvarg (val_interp sign ast)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b68196ff3b..d63325cd85 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -58,12 +58,14 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
-let pf_get_hyp_typ gls id = 
+let pf_get_hyp gls id = 
   try 
-    body_of_type (snd (lookup_id id (pf_hyps gls)))
+    lookup_id id (pf_hyps gls)
   with Not_found -> 
     error ("No such hypothesis : " ^ (string_of_id id))
 
+let pf_get_hyp_typ gls id = snd (pf_get_hyp gls id)
+
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
 let pf_ctxt gls      = get_ctxt (sig_it gls)
@@ -229,9 +231,17 @@ let convert_concl c pf =
   refiner (Prim { name = Convert_concl; terms = [c];
                   hypspecs = []; newids = []; params = [] }) pf
 
-let convert_hyp id c pf = 
+let convert_hyp id t pf =
   refiner (Prim { name = Convert_hyp; hypspecs = [id];
-                  terms = [c]; newids = []; params = []}) pf
+                  terms = [t]; newids = []; params = []}) pf
+
+let convert_defbody id t pf =
+  refiner (Prim { name = Convert_defbody; hypspecs = [id];
+                  terms = [t]; newids = []; params = []}) pf
+
+let convert_deftype id t pf =
+  refiner (Prim { name = Convert_deftype; hypspecs = [id];
+                  terms = [t]; newids = []; params = []}) pf
 
 let thin ids gl = 
   refiner (Prim { name = Thin; hypspecs = ids;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 5481491d53..e7742f2ecd 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -56,7 +56,8 @@ val hnf_type_of           : goal sigma -> constr -> constr
 val pf_interp_constr      : goal sigma -> Coqast.t -> constr
 val pf_interp_type        : goal sigma -> Coqast.t -> constr
 
-val pf_get_hyp_typ        : goal sigma -> identifier -> constr 
+val pf_get_hyp            : goal sigma -> identifier -> constr option * types
+val pf_get_hyp_typ        : goal sigma -> identifier -> types
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
@@ -162,7 +163,9 @@ val introduction    : identifier -> tactic
 val intro_replacing : identifier -> tactic
 val refine          : constr -> tactic
 val convert_concl   : constr -> tactic
-val convert_hyp     : identifier -> constr -> tactic
+val convert_hyp     : identifier -> types -> tactic
+val convert_deftype : identifier -> types -> tactic
+val convert_defbody : identifier -> constr -> tactic
 val thin            : identifier list -> tactic
 val move_hyp        : bool -> identifier -> identifier -> tactic
 val mutual_fix      : identifier list -> int list -> constr list -> tactic
@@ -228,7 +231,7 @@ val hide_openconstr_tactic  : Pretyping.open_constr hide_combinator
 val hide_constrl_tactic : (constr list) hide_combinator
 val hide_numarg_tactic  : int hide_combinator
 val hide_ident_tactic   : identifier hide_combinator
-val hide_identl_tactic  : (identifier list) hide_combinator
+val hide_identl_tactic  : hyp_location list hide_combinator
 val hide_string_tactic  : string hide_combinator
 val hide_bindl_tactic   : ((bindOcc * constr) list) hide_combinator
 val hide_cbindl_tactic  : (constr * (bindOcc * constr) list) hide_combinator
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. *)