correction Abstract (et make world passe!)

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

3 files changed, 21 insertions, 13 deletions

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 962c18cc17..d562b0ed90 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -188,15 +188,21 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ind =
     try find_rectype env sigma i
     with Induc ->
-      errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in
+      errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) 
+  in
   let (invEnv,invGoal) =
-    compute_first_inversion_scheme env sigma ind sort dep_option in
-  assert (list_subset (global_vars invGoal) (ids_of_named_context (named_context invEnv)));
-(*
+    compute_first_inversion_scheme env sigma ind sort dep_option 
+  in
+  assert 
+    (list_subset 
+       (global_vars invGoal) 
+       (ids_of_named_context (named_context invEnv)));
+  (*
     errorlabstrm "lemma_inversion"
-      [< 'sTR"Computed inversion goal was not closed in initial signature" >];
-*)
-  let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invEnv invGoal) in
+    [< 'sTR"Computed inversion goal was not closed in initial signature" >];
+  *)
+  let invSign = named_context invEnv in
+  let pfs = mk_pftreestate (mk_goal (mt_ctxt Intset.empty) invSign invGoal) in
   let pfs =
     solve_pftreestate (tclTHEN intro 
 			 (onLastHyp (compose inv_op out_some))) pfs in
@@ -207,16 +213,19 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       (fun env (id,_,_ as d) sign ->
          if mem_named_context id global_named_context then sign
 	 else add_named_decl d sign)
-      invEnv empty_named_context in
+      invEnv empty_named_context 
+  in
   let (_,ownSign,mvb) =
     List.fold_left
       (fun (avoid,sign,mvb) (mv,mvty) ->
          let h = next_ident_away (id_of_string "H") avoid in
 	 (h::avoid, add_named_assum (h,mvty) sign, (mv,mkVar h)::mvb))
       (ids_of_context invEnv, ownSign, [])
-      meta_types in
+      meta_types 
+  in
   let invProof = 
-    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign in
+    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign 
+  in
   invProof
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5a5500fdc6..018197dd49 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -120,7 +120,7 @@ let pf_is_matching gls pat n =
   is_matching_conv (w_env wc) (w_Underlying wc) pat n
 
 let pf_matches gls pat n =
-  matches_conv (sig_it gls).Evd.evar_env (Stamps.ts_it (sig_sig gls)) pat n
+  matches_conv (pf_env gls) (Stamps.ts_it (sig_sig gls)) pat n
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 34ad6e56cd..8b9a8d0af1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1653,9 +1653,8 @@ let abstract_subproof name tac gls =
              (ids_of_named_context global_sign) in
   let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t)
                 (pf_concl gls) sign in
-  let env' = change_hyps (fun _ -> current_sign) env in
   let lemme =
-    start_proof na Declare.NeverDischarge env' concl;
+    start_proof na Declare.NeverDischarge current_sign concl;
     let _,(const,strength) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));