Prise en compte de Let à certains endroits

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

1 files changed, 6 insertions, 12 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9fb5cc6c52..ed5406b79c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -65,11 +65,8 @@ let dest_match_eq gls eqn =
 	    [< 'sTR "no primitive equality here" >]))
     
 (* Environment management *)
-let push_rel_type sigma (na,t) env =
-  push_rel_decl (na,make_typed t (get_sort_of env sigma t)) env
-
 let push_rels vars env =
-  List.fold_right (push_rel_type Evd.empty) vars env
+  List.fold_right push_rel vars env
 
 type inversion_status = Dep of constr option | NoDep
 
@@ -85,7 +82,6 @@ let make_inv_predicate env sigma ind id status concl =
       | NoDep ->
 	  (* We push the arity and leave concl unchanged *)
 	  let hyps_arity,_ = get_arity indf in
-	  let env' = push_rels hyps_arity env in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (dependent (mkVar id) concl) then
@@ -100,12 +96,10 @@ let make_inv_predicate env sigma ind id status concl =
               | None ->
 		let sort = get_sort_of env sigma concl in
 		let p = make_arity env true indf sort in
-		abstract_list_all env sigma p concl (realargs@[mkVar id])
-	  in
-	  let hyps,_ = decompose_lam_n (nrealargs+1) pred in
-	  let c3 = whd_beta (applist (pred,rel_list nrealargs (nrealargs +1))) 
-	  in
-	  (hyps,c3)
+		abstract_list_all env sigma p concl (realargs@[mkVar id]) in
+	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
+	  (* We lift to make room for the equations *)
+	  (hyps,lift nrealargs bodypred)
   in
   let nhyps = List.length hyps in
   let env' = push_rels hyps env in
@@ -132,7 +126,7 @@ let make_inv_predicate env sigma ind id status concl =
 	build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
   in
   let (newconcl,neqns) = build_concl [] 0 pairs in
-  let predicate = it_lambda_name env newconcl hyps in
+  let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   (predicate,neqns)