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

7 files changed, 103 insertions, 20 deletions

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