diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-04 09:01:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-04 09:01:11 +0000 |
| commit | f0ef4e792d41249921eabe951b73fbc8c956484e (patch) | |
| tree | 83101451359af57e7f952b58bec37109755f646f /tactics/tacinterp.ml | |
| parent | 9728a4b50d3c7da120cd384bb2eb3dcc02bd7585 (diff) | |
Confusion message erreur détectée par nouveau warning X de ocaml 3.09
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c27e35dad..79b3b330d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1567,8 +1567,7 @@ and interp_match_context ist g lz lr lmr = | PatternMatchingFailure -> apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" (str - "No matching clauses for match goal") + errorlabstrm "Tacinterp.apply_match_context" (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Debug On\" for more info)" |