diff options
| -rwxr-xr-x | theories/Arith/Gt.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Le.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Lt.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Min.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Minus.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Mult.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Peano_dec.v | 4 | ||||
| -rwxr-xr-x | theories/Arith/Plus.v | 2 | ||||
| -rwxr-xr-x | theories/Arith/Wf_nat.v | 2 | ||||
| -rwxr-xr-x | theories/Bool/Bool.v | 8 | ||||
| -rwxr-xr-x | theories/Bool/DecBool.v | 6 | ||||
| -rwxr-xr-x | theories/Bool/IfProp.v | 2 | ||||
| -rw-r--r-- | theories/Bool/Sumbool.v | 2 | ||||
| -rwxr-xr-x | theories/Bool/Zerob.v | 2 |
14 files changed, 20 insertions, 20 deletions
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index f2e27e7bfc..f31154018e 100755 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Le. Require Lt. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 7766d3d7e4..be420c6721 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (***************************************) (* Order on natural numbers *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index aa4ad4950b..7856850934 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Le. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 8f9eb5ecde..bc976fbd25 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Arith. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index afb5a19844..3da5916e04 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (**************************************************************************) diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index e90cec6612..8955b1ea31 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Plus. Require Export Minus. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 5ee33d1563..b02d5a324c 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Decidable. -(* $Id$ *) +(*i $Id$ i*) +Require Decidable. Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. Proof. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index c070e3645e..67121590ee 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (**************************************************************************) (* Properties of addition *) diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 041d243495..2f100ebc52 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* Well-founded relations and natural numbers *) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 459c145e17..4f7df44fd0 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (*************) -(*s Booleans *) +(* Booleans *) (* The type [bool] is defined in the prelude as \\ - [Inductive bool : Set := true : bool | false : bool (from Prelude)] *) + [Inductive bool : Set := true : bool | false : bool] *) -(*s Interpretation of booleans as Propopsition *) +(* Interpretation of booleans as Proposition *) Definition Is_true := [b:bool](Cases b of true => True | false => False diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 59278ec11d..8daabd4793 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. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index f4c4d4cb4f..bcbe0f7140 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Bool. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 749accdd47..e91b3fb1a6 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* Here are collected some results about the type sumbool (see INIT/Specif.v) * diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index b36fc94d5a..8a8d096215 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Arith. Require Bool. |