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

1 files changed, 14 insertions, 4 deletions

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;