aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.mli
diff options
context:
space:
mode:
authorglondu2009-09-17 15:58:14 +0000
committerglondu2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /proofs/logic.mli
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/logic.mli')
-rw-r--r--proofs/logic.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 8bc48ed54f..0d56da382a 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,9 +26,9 @@ val with_check : tactic -> tactic
[Intro]: no check that the name does not exist\\
[Intro_after]: no check that the name does not exist and that variables in
its type does not escape their scope\\
- [Intro_replacing]: no check that the name does not exist and that
+ [Intro_replacing]: no check that the name does not exist and that
variables in its type does not escape their scope\\
- [Convert_hyp]:
+ [Convert_hyp]:
no check that the name exist and that its type is convertible\\
*)