diff options
| -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 |