diff options
| author | Hugo Herbelin | 2014-10-07 14:09:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 14:44:27 +0200 |
| commit | 376a6b66bf4c4181214bb86a07c4677f17112b4c (patch) | |
| tree | 9909c9bfd0570bb7ab95c477ed87b9bcc24b6240 | |
| parent | aeb20a17562fde5c07bd398da589d721e8c0aabf (diff) | |
Removing debugging information committed by mistake.
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cc95430f5a..c40dc40786 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -476,9 +476,9 @@ let weak_check env sigma deep newc origc = let change_and_check cv_pb deep t env sigma c = let sigma, t' = t env sigma in let b = weak_check env sigma deep t' c in - if not b then errorlabstrm "convert-check-hyp" (str "Not convertible1."); + if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then errorlabstrm "convert-check-hyp" (str "Not convertible2."); + if not b then errorlabstrm "convert-check-hyp" (str "Not convertible."); sigma, t' let change_and_check_subst cv_pb subst t env sigma c = |