diff options
| author | sacerdot | 2004-08-24 09:19:06 +0000 |
|---|---|---|
| committer | sacerdot | 2004-08-24 09:19:06 +0000 |
| commit | 258f9d3ed4a9f28277ea4fdd7463290c39104a82 (patch) | |
| tree | 5bd8c2d9736ddff2e21b61f8bbb04ebdd2431b8a | |
| parent | ade77a758870c9becf61a3f3348f128594de62d7 (diff) | |
Calling setoid_rewrite on a term H whose type (eq x y) was not an application
of a setoid equality was erroneously considered an assertion failure instead
of an user error.
Note: in this case the tactic should try the rewrite tactic. However, since
rewrite recursively calls setoid_rewrite in this case, this solution can
diverge. This will be fixed in a future commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6028 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 44203278b3..4a44e72d29 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -681,7 +681,11 @@ let mark_occur gl hyp = | [_;_] -> [] | he::tl -> he::(get_all_but_last_two tl) in let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in - try setoid_table_find aeq with Not_found -> assert false + try + setoid_table_find aeq + with Not_found -> + errorlabstrm "Setoid_rewrite" + (prterm aeq ++ str " is not a setoid equality.") in Toreplace sa else |