aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/BoolEq.v
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-15 19:48:24 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-15 19:48:24 +0000
commit3675bac6c38e0a26516e434be08bc100865b339b (patch)
tree87f8eb1905c7b508dea60b1e216f79120e9e772d /theories/Bool/BoolEq.v
parentc881bc37b91a201f7555ee021ccb74adb360d131 (diff)
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/BoolEq.v')
-rw-r--r--theories/Bool/BoolEq.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index ef48e6272..1baa54241 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -70,4 +70,4 @@ Section Bool_eq_dec.
right; apply beq_false_not_eq; assumption.
Defined.
-End Bool_eq_dec. \ No newline at end of file
+End Bool_eq_dec.