diff options
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8d9d9e0308..cc1581296b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -559,7 +559,7 @@ let find_matching_clause unifier clause = try unifier clause with exn when catchable_exception exn -> try find (clenv_push_prod clause) - with NotExtensibleClause -> error "Cannot apply" + with NotExtensibleClause -> failwith "Cannot apply" in find clause let apply_in_once gls innerclause (d,lbind) = |