aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/DecBool.v
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 12:25:05 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-19 12:25:05 +0000
commitbdbbb1bea47909ad5d0daffd77e090ef9b59d826 (patch)
tree4d1265dfb29299fb395a554a3b32eb550b4662a2 /theories/Bool/DecBool.v
parent45aa164112c77d61f726d5db32041c9518ed378a (diff)
Mise de (*i autour CVS info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/DecBool.v')
-rwxr-xr-xtheories/Bool/DecBool.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 59278ec11..8daabd479 100755
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id$ *)
+(*i $Id$ i*)
-Implicit Arguments On.
+Set Implicit Arguments.
Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
:= [A,B,C,H,x,y]if H then [_]x else [_]y.
@@ -24,4 +24,4 @@ Intros; Case H; Auto.
Intro; Absurd A; Trivial.
Save.
-Implicit Arguments Off.
+Unset Implicit Arguments.