- 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

6 files changed, 24 insertions, 50 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0d4cdfe5ab..63accefd11 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -161,9 +161,9 @@ let pr_rel_decl env (na,c,typ) =
 
 (* Prints a signature, all declarations on the same line if possible *)
 let pr_named_context_of env =
-  hv 0 (fold_named_context
-	  (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
-          env ~init:(mt ()))
+  let make_decl_list env d pps = pr_var_decl env d :: pps in
+  let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
+  hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_named_context env ne_context = 
   hv 0 (Sign.fold_named_context
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
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5d02e621d2..e0ed2d1ef4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -482,32 +482,14 @@ let raw_inversion inv_kind id status names gl =
   gl
 
 (* Error messages of the inversion tactics *)
-let not_found_message ids =
-  if List.length ids = 1 then
-    (str "the variable" ++ spc () ++ str (string_of_id (List.hd ids)) ++ spc () ++
-      str" was not found in the current environment")
-  else 
-    (str "the variables [" ++ 
-      spc () ++ prlist (fun id -> (str (string_of_id id) ++ spc ())) ids ++
-      str" ] were not found in the current environment")
-
-let dep_prop_prop_message id =
-  errorlabstrm "Inv"
-    (str "Inversion on " ++ pr_id id ++
-       str " would need dependent elimination from Prop to Prop.")
- 
-let not_inductive_here id =
-  errorlabstrm "mind_specif_of_mind"
-    (str "Cannot recognize an inductive predicate in " ++ pr_id id ++
-       str ". If there is one, may be the structure of the arity or of the type of constructors is hidden by constant definitions.")
-
-(* Noms d'errreurs obsolètes ?? *)
 let wrap_inv_error id = function
-  | UserError ("Case analysis",s) -> errorlabstrm "Inv needs Nodep Prop Set" s
-  | UserError("mind_specif_of_mind",_)  -> not_inductive_here id
-  | UserError (a,b)  -> errorlabstrm "Inv" b
-  | Invalid_argument "List.fold_left2" -> dep_prop_prop_message id
-  | Not_found  ->  errorlabstrm "Inv" (not_found_message [id]) 
+  | Indrec.RecursionSchemeError
+      (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
+      errorlabstrm ""
+	(strbrk "Inversion would require case analysis on sort " ++
+	pr_sort k ++ 
+	strbrk " which is not allowed for inductive definition " ++
+	pr_inductive (Global.env()) i ++ str ".")
   | e -> raise e
 
 (* The most general inversion tactic *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f760e731ba..26c29d4c0f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -655,17 +655,13 @@ let error_not_an_arity id =
 let error_bad_entry () =
   str "Bad inductive definition."
 
-let error_not_allowed_case_analysis dep kind i =
-  str (if dep then "Dependent" else "Non dependent") ++
-  str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++
-  str "is not allowed for inductive definition: " ++
-  pr_inductive (Global.env()) i ++ str "."
+(* Recursion schemes errors *)
 
-let error_bad_induction dep indid kind =
-  str (if dep then "Dependent" else "Non dependent") ++
-  str " induction for type " ++ pr_id indid ++
-  str " and sort " ++ pr_sort kind ++ spc () ++
-  str "is not allowed."
+let error_not_allowed_case_analysis isrec kind i =
+  str (if isrec then "Induction" else "Case analysis") ++
+  strbrk " on sort " ++ pr_sort kind ++ 
+  strbrk " is not allowed for inductive definition " ++
+  pr_inductive (Global.env()) i ++ str "."
 
 let error_not_mutual_in_scheme ind ind' =
   if ind = ind' then
@@ -693,9 +689,8 @@ let explain_inductive_error = function
 (* Recursion schemes errors *)
 
 let explain_recursion_scheme_error = function
-  | NotAllowedCaseAnalysis (dep,k,i) ->
-      error_not_allowed_case_analysis dep k i
-  | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
+  | NotAllowedCaseAnalysis (isrec,k,i) ->
+      error_not_allowed_case_analysis isrec k i
   | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
 
 (* Pattern-matching errors *)