- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in

  Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk 
  revision 11300).
- Improved various error messages related to inversion, evars and case 
  analysis (including the removal of the obsolete dependent/non dependent
  distinction).



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

3 files changed, 6 insertions, 9 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fafdfe9950..733aa9613b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -431,7 +431,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 		     has dependencies in another hyp of the context of ev
 		     and transitively remember the dependency *)
 		  match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
-		  | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri)
+		  | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
 		  | _ ->
 		  (* No dependency at all, we can keep this ev's context hyp *)
 		      (h::hy,a::ar,ri))
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ffbc9debc1..996c00ebaf 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -29,8 +29,7 @@ open Sign
 
 (* Errors related to recursors building *)
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
   | NotMutualInScheme of inductive * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
@@ -57,8 +56,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
-	 (NotAllowedCaseAnalysis
-	    (dep,(new_sort_in_family kind),ind)));
+	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
 
   let ndepar = mip.mind_nrealargs + 1 in
 
@@ -502,10 +500,10 @@ let instantiate_type_indrec_scheme sort npars term =
 let check_arities listdepkind = 
   let _ = List.fold_left
     (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> 
-       let id = mipi.mind_typename  in
        let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
-	 (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind)))
+	 (RecursionSchemeError
+	   (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
        else if List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index b172935f58..d7507bd66c 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -20,8 +20,7 @@ open Evd
 (* Errors related to recursors building *)
 
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
   | NotMutualInScheme of inductive * inductive
 
 exception RecursionSchemeError of recursion_scheme_error