bugs

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

2 files changed, 9 insertions, 12 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1e3770ad0..86eb8113e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1200,7 +1200,7 @@ let subst_tuple_term env sigma dep_pair b =
   strong (fun _ _ -> 
 	    compose (whd_betaiota env sigma)
 	      (whd_const [proj1_sp;proj2_sp;sig_elim_sp] env sigma)) 
-    env sigma*) app_B
+    env sigma*) whd_betaiota env sigma app_B
     
 (* |- (P e2)
      BY RevSubstInConcl (eq T e1 e2)
@@ -1210,7 +1210,7 @@ let subst_tuple_term env sigma dep_pair b =
 let revSubstInConcl eqn gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
   let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in
-  assert (not (dependent (Rel 1) body));
+  assert (dependent (Rel 1) body);
   bareRevSubstInConcl lbeq body (t,e1,e2) gls
 
 (* |- (P e1)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index cd8fa4926..587890ca5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -136,20 +136,17 @@ let make_inv_predicate env sigma ind id status concl =
 	    whd_beta env sigma
 	      (applist (pred,rel_list nrealargs (nrealargs +1))) 
 	  in
-
-
-		(hyps,c3)
+	  (hyps,c3)
   in
-  let n = List.length hyps in
-  let env' = push_rels hyps env in
-  let realargs' = List.map (lift n) realargs in
-  let pairs = list_map_i (compute_eqn env' sigma n) 0 realargs' in
   let nhyps = List.length hyps in
+  let env' = push_rels hyps env in
+  let realargs' = List.map (lift nhyps) realargs in
+  let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,Rel(n-i+1) *)
   (* Now, we can recurse down this list, for each ai,(Rel k) whether to
      push <Ai>(Rel k)=ai (when   Ai is closed).
-   In any case, we carry along the rest of larg_var_list *)
+   In any case, we carry along the rest of pairs *)
   let rec build_concl eqns n = function
     | [] -> (prod_it concl eqns,n)
     | ((ai,ati),(xi,ti))::restlist ->
@@ -163,9 +160,9 @@ let make_inv_predicate env sigma ind id status concl =
         let sort = get_sort_of env sigma concl in 
         let eq_term = find_eq_pattern type_type_rhs sort in
         let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in 
-	build_concl ((Anonymous,lift n eqn)::hyps) (n+1) restlist
+	build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
   in
-  let (newconcl,neqns) = build_concl hyps 0 pairs in
+  let (newconcl,neqns) = build_concl [] 0 pairs in
   let predicate = it_lambda_name env newconcl hyps in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)