Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix permet)

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

1 files changed, 18 insertions, 4 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c2578cdd74..b4af4821d9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -306,15 +306,29 @@ and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) =
     if n = 0 then
       let c = detype tenv avoid env c in
       let t = detype tenv avoid env t in
-      List.fold_left (fun c (na,t) -> RLambda (dummy_loc,na,t,c)) c l,
-      List.fold_left (fun c (na,t) -> RProd (dummy_loc,na,t,c)) t l
+      List.fold_left (fun (c,typ) (na,body,t) -> match body with
+	| None -> (RLambda (dummy_loc,na,t,c),RProd (dummy_loc,na,t,typ))
+	| Some b -> (RLetIn (dummy_loc,na,b,c),RLetIn (dummy_loc,na,b,typ)))
+	(c,t) l
     else match kind_of_term c, kind_of_term t with
       | Lambda (na,t,c), Prod (_,t',c') ->
           let t = detype tenv avoid env t in
 	  let id = next_name_away na avoid in 
           let avoid = id::avoid and env = add_name (Name id) env in
-          share_names (n-1) ((na,t)::l) avoid env c c'
-      | _ -> anomaly "Detype: wrong fix" in
+          share_names (n-1) ((na,None,t)::l) avoid env c c'
+      (* May occur for fix built interactively *)
+      | LetIn (na,b,t',c), _ ->
+          let t' = detype tenv avoid env t' in
+          let b = detype tenv avoid env b in
+	  let id = next_name_away na avoid in 
+          let avoid = id::avoid and env = add_name (Name id) env in
+          share_names n ((na,Some b,t')::l) avoid env c t
+      (* Only if built with the f/n notation or w/o let-expansion in types *)
+      | _, LetIn (_,b,_,t) ->
+	  share_names n l avoid env c (subst1 b t)
+      (* If built with the f/n notation or in an open proof: we renounce to *)
+      (* share names *)
+      | _ -> share_names 0 l avoid env c t in
   let n = Array.length tys in
   let v = array_map3
     (fun c t i -> share_names (i+1) [] def_avoid def_env c (lift n t))