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

3 files changed, 25 insertions, 5 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 299c061c9..e9892758b 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -256,12 +256,16 @@ let rec ast_of_raw = function
 	 | RFix (nv,n) ->
              let rec split_lambda binds = function
 	       | (0, t) -> (binds,ast_of_raw t)
+	       | (n, RLetIn (_,na,b,c)) ->
+		   let bind = ope("LETBINDER",[ast_of_raw b;ast_of_name na]) in
+		   split_lambda (bind::binds) (n,c)
 	       | (n, RLambda (_,na,t,b)) ->
 		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
 		   split_lambda (bind::binds) (n-1,b)
 	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
 	     let rec split_product = function
 	       | (0, t) -> ast_of_raw t
+	       | (n, RLetIn (_,na,_,c)) -> split_product (n,c)
 	       | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
 	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
 	     let listdecl = 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c2578cdd7..b4af4821d 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))
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 0b111a69f..492c5cbba 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -33,7 +33,9 @@ Syntax constr
   | bindersone  [ << (BINDERS (BINDER $c ($LIST $id))) >> ] -> 
        [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
 
-  | letbinder  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
+  | letbindercons [ << (BINDERS (LETBINDER $c $id) ($LIST $b)) >> ] ->
+       [ [<hov 0> id ":=" [0 1] $c:E ";" [1 0] (BINDERS ($LIST $b)) ] ]
+  | letbinderone  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
        [ [<hov 0> id ":=" [0 1] $c:E ] ]
   ;