diff options
| author | herbelin | 2006-10-26 07:52:31 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-26 07:52:31 +0000 |
| commit | fb147ff4928c1720492693d61f97c49a84839bc0 (patch) | |
| tree | cfdab758c9ecceaa91eac1f11a2b58b27fa5a16b | |
| parent | 32f5e926ed646fcdba6ae45141d2a6d5b3ae738a (diff) | |
Petit bug apply in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9281 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) = |