Amélioration des messages d'erreurs de tacred; unfold considère maintenant le

prédicat de filtrage après le terme filtré conformément à l'affichage


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

4 files changed, 39 insertions, 14 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ef0867f7c4..10322c156c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,15 @@ open Closure
 open Cbv
 open Rawterm
 
+(* Errors *)
+
+type reduction_tactic_error = 
+    InvalidAbstraction of env * constr * (env * Type_errors.type_error)
+
+exception ReductionTacticError of reduction_tactic_error
+
+(* Evaluable reference *)
+
 exception Elimconst
 exception Redelimination
 
@@ -619,7 +628,7 @@ let contextually byhead (locs,c) f env sigma t =
   in
   let t' = traverse (env,c) t in
   if locs <> [] & List.exists (fun o -> o >= !pos or o <= - !pos) locs then
-    errorlabstrm "contextually" (str "Too few occurences");
+    error_invalid_occurrence locs;
   t'
 
 (* linear bindings (following pretty-printer) of the value of name in c.
@@ -683,7 +692,7 @@ let rec substlin env name n ol c =
                let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
                (n2,ol2,mkProd (na,c1',c2')))
 	
-    | Case (ci,p,d,llf) -> 
+    | Case (ci,p,d,llf) ->
         let rec substlist nn oll = function
           | []     -> (nn,oll,[])
           | f::lfe ->
@@ -694,11 +703,12 @@ let rec substlin env name n ol c =
                      let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in
                      (nn2,oll2,f'::lfe'))
 	in
-	let (n1,ol1,p') = substlin env name n ol p in  (* ATTENTION ERREUR *)
-        (match ol1 with                                 (* si P pas affiche *)
-           | [] -> (n1,[],mkCase (ci, p', d, llf))
+	(* p is printed after d in v8 syntax *)
+	let (n1,ol1,d') = substlin env name n ol d in
+        (match ol1 with
+           | [] -> (n1,[],mkCase (ci, p, d', llf))
            | _  ->
-               let (n2,ol2,d') = substlin env name n1 ol1 d in
+               let (n2,ol2,p') = substlin env name n1 ol1 p in
                (match ol2 with
 		  | [] -> (n2,[],mkCase (ci, p', d', llf))
 		  | _  -> 
@@ -746,8 +756,8 @@ let unfoldoccs env sigma (occl,name) c =
           | (_,[],uc) -> nf_betaiota uc
           | (1,_,_) ->
               error ((string_of_evaluable_ref env name)^" does not occur")
-          | _ -> error ("bad occurrence numbers of "
-			^(string_of_evaluable_ref env name))
+          | (_,l,_) ->
+	      error_invalid_occurrence l
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c = 
@@ -790,8 +800,11 @@ let abstract_scheme env sigma (locc,a) c =
 
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
-  let _ = Typing.type_of env sigma abstr_trm in
-  applist(abstr_trm, List.map snd loccs_trm)
+  try
+    let _ = Typing.type_of env sigma abstr_trm in
+    applist(abstr_trm, List.map snd loccs_trm)
+  with Type_errors.TypeError (env',t) ->
+    raise (ReductionTacticError (InvalidAbstraction (env,abstr_trm,(env',t))))
 
 (* Used in several tactics. *)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 423a04723d..9ffa1dfb76 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -18,6 +18,11 @@ open Closure
 open Rawterm
 (*i*)
 
+type reduction_tactic_error = 
+    InvalidAbstraction of env * constr * (env * Type_errors.type_error)
+
+exception ReductionTacticError of reduction_tactic_error
+
 (*s Reduction functions associated to tactics. \label{tacred} *)
 
 val is_evaluable : env -> evaluable_global_reference -> bool
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 95bdb74c51..597ddac57c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -615,6 +615,11 @@ let replace_term = replace_term_gen eq_constr
    bindings is done. The list may contain only negative occurrences
    that will not be substituted. *)
 
+let error_invalid_occurrence l =
+  errorlabstrm ""
+    (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ 
+     prlist_with_sep spc int l)
+
 let subst_term_occ_gen locs occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
@@ -646,8 +651,8 @@ let subst_term_occ locs c t =
     t
   else 
     let (nbocc,t') = subst_term_occ_gen locs 1 c t in
-    if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
-      errorlabstrm "subst_term_occ" (str "Too few occurences");
+    let rest = List.filter (fun o -> o >= nbocc or o <= -nbocc) locs in
+    if rest <> [] then error_invalid_occurrence rest;
     t'
 
 let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
@@ -661,8 +666,8 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
 	else 
 	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
 	  let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
-	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
-	    errorlabstrm "subst_term_occ_decl" (str "Too few occurences");
+	  let rest = List.filter (fun o -> o >= nbocc' or o <= -nbocc') locs in
+	  if rest <> [] then error_invalid_occurrence rest;
 	  (id,Some body',t')
 
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index cd1cce1bae..5ecd0b685f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -124,6 +124,8 @@ val subst_term_occ : int list -> constr -> types -> types
 val subst_term_occ_decl :
   int list -> constr -> named_declaration -> named_declaration
 
+val error_invalid_occurrence : int list -> 'a
+
 (* Alternative term equalities *)
 val eta_reduce_head : constr -> constr
 val eta_eq_constr : constr -> constr -> bool