diff options
| author | herbelin | 2006-02-07 22:11:50 +0000 |
|---|---|---|
| committer | herbelin | 2006-02-07 22:11:50 +0000 |
| commit | 634e6ddaecc6f6bf577c39d6b146e7d75fb79c74 (patch) | |
| tree | e72b848a7fa7f74efd00aec93062cf38a0365fc7 /pretyping/termops.ml | |
| parent | b4d90fd1babe9a78dae9431aa466a197625bf3d6 (diff) | |
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
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 13 |
1 files changed, 9 insertions, 4 deletions
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') |