From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 4e28b5b905..f5e936cf01 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -19,7 +19,7 @@ Require Export DoubleType. arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, - 63-bit integers is now just a matter of replacing every occurences + 63-bit integers is now just a matter of replacing every occurrences of 31 by 63. This is actually made possible by the use of dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 6fdf0a2a5b..376620ddcd 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -15,7 +15,7 @@ Require Import List. (** * Generic dependently-typed operators about [n]-ary functions *) (** The type of [n]-ary function: [nfun A n B] is - [A -> ... -> A -> B] with [n] occurences of [A] in this type. *) + [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *) Fixpoint nfun A n B := match n with -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/NatInt/NZDiv.v | 2 +- theories/Numbers/Natural/Abstract/NDiv.v | 2 +- theories/Numbers/Natural/Abstract/NParity.v | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d0df8fb4a7..ab73ebfe1d 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index d5f3f4ada7..c8260e516f 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index de2e99ec3a..464fe354b8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -404,7 +404,7 @@ Proof. intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto. Qed. -(** Some additionnal inequalities about quot. *) +(** Some additional inequalities about quot. *) Theorem quot_lt_upper_bound: forall a b q, 0<=a -> 0 a < b*q -> a÷b < q. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 4a127216f8..e0dfdedbd5 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -307,7 +307,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0 a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index fb68c139b5..d3d3eb0fbb 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -137,7 +137,7 @@ Proof. intros; apply mul_succ_div_gt; auto'. Qed. Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). Proof. intros. apply div_exact; auto'. Qed. -(** Some additionnal inequalities about div. *) +(** Some additional inequalities about div. *) Theorem div_lt_upper_bound: forall a b q, b~=0 -> a < b*q -> a/b < q. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index b3526c9a17..80a579f19f 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -8,7 +8,7 @@ Require Import Bool NSub NZParity. -(** Some additionnal properties of [even], [odd]. *) +(** Some additional properties of [even], [odd]. *) Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- theories/Numbers/BigNumPrelude.v | 2 +- theories/Numbers/BinNums.v | 2 +- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 +- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v | 2 +- theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 2 +- theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 +- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/Cyclic/Int31/Ring31.v | 2 +- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 2 +- theories/Numbers/Integer/Abstract/ZAdd.v | 2 +- theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +- theories/Numbers/Integer/Abstract/ZBase.v | 2 +- theories/Numbers/Integer/Abstract/ZBits.v | 2 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/Integer/Abstract/ZGcd.v | 2 +- theories/Numbers/Integer/Abstract/ZLcm.v | 2 +- theories/Numbers/Integer/Abstract/ZLt.v | 2 +- theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +- theories/Numbers/Integer/Abstract/ZMul.v | 2 +- theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZParity.v | 2 +- theories/Numbers/Integer/Abstract/ZPow.v | 2 +- theories/Numbers/Integer/Abstract/ZProperties.v | 2 +- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +- theories/Numbers/Integer/BigZ/BigZ.v | 2 +- theories/Numbers/Integer/BigZ/ZMake.v | 2 +- theories/Numbers/Integer/Binary/ZBinary.v | 2 +- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 2 +- theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +- theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- theories/Numbers/NatInt/NZAdd.v | 2 +- theories/Numbers/NatInt/NZAddOrder.v | 2 +- theories/Numbers/NatInt/NZAxioms.v | 2 +- theories/Numbers/NatInt/NZBase.v | 2 +- theories/Numbers/NatInt/NZBits.v | 2 +- theories/Numbers/NatInt/NZDiv.v | 2 +- theories/Numbers/NatInt/NZDomain.v | 2 +- theories/Numbers/NatInt/NZGcd.v | 2 +- theories/Numbers/NatInt/NZLog.v | 2 +- theories/Numbers/NatInt/NZMul.v | 2 +- theories/Numbers/NatInt/NZMulOrder.v | 2 +- theories/Numbers/NatInt/NZOrder.v | 2 +- theories/Numbers/NatInt/NZParity.v | 2 +- theories/Numbers/NatInt/NZPow.v | 2 +- theories/Numbers/NatInt/NZProperties.v | 2 +- theories/Numbers/NatInt/NZSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NAdd.v | 2 +- theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +- theories/Numbers/Natural/Abstract/NAxioms.v | 2 +- theories/Numbers/Natural/Abstract/NBase.v | 2 +- theories/Numbers/Natural/Abstract/NBits.v | 2 +- theories/Numbers/Natural/Abstract/NDefOps.v | 2 +- theories/Numbers/Natural/Abstract/NDiv.v | 2 +- theories/Numbers/Natural/Abstract/NGcd.v | 2 +- theories/Numbers/Natural/Abstract/NIso.v | 2 +- theories/Numbers/Natural/Abstract/NLcm.v | 2 +- theories/Numbers/Natural/Abstract/NLog.v | 2 +- theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +- theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +- theories/Numbers/Natural/Abstract/NOrder.v | 2 +- theories/Numbers/Natural/Abstract/NParity.v | 2 +- theories/Numbers/Natural/Abstract/NPow.v | 2 +- theories/Numbers/Natural/Abstract/NProperties.v | 2 +- theories/Numbers/Natural/Abstract/NSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +- theories/Numbers/Natural/Abstract/NSub.v | 2 +- theories/Numbers/Natural/BigN/BigN.v | 2 +- theories/Numbers/Natural/BigN/NMake.v | 2 +- theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +- theories/Numbers/Natural/BigN/Nbasic.v | 2 +- theories/Numbers/Natural/Binary/NBinary.v | 2 +- theories/Numbers/Natural/Peano/NPeano.v | 2 +- theories/Numbers/Natural/SpecViaZ/NSig.v | 2 +- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 +- theories/Numbers/NumPrelude.v | 2 +- theories/Numbers/Rational/BigQ/BigQ.v | 2 +- theories/Numbers/Rational/BigQ/QMake.v | 2 +- theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +- 90 files changed, 90 insertions(+), 90 deletions(-) (limited to 'theories/Numbers') diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 6817947c8c..45a7527c97 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr:true + | nil => constr:(true) | ?t::?l => match t with | D1 => isInt31cst_lst l | D0 => isInt31cst_lst l - | _ => constr:false + | _ => constr:(false) end - | _ => constr:false + | _ => constr:(false) end. Ltac isInt31cst t := @@ -38,17 +38,17 @@ Ltac isInt31cst t := ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20 ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil) in isInt31cst_lst l - | Int31.On => constr:true - | Int31.In => constr:true - | Int31.Tn => constr:true - | Int31.Twon => constr:true - | _ => constr:false + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) end. Ltac Int31cst t := match isInt31cst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** The generic ring structure inferred from the Cyclic structure *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index ec495d0947..56cb9bbc2c 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -148,26 +148,26 @@ Ltac isBigZcst t := match t with | BigZ.Pos ?t => isBigNcst t | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:true - | BigZ.one => constr:true - | BigZ.two => constr:true - | BigZ.minus_one => constr:true - | _ => constr:false + | BigZ.zero => constr:(true) + | BigZ.one => constr:(true) + | BigZ.two => constr:(true) + | BigZ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigZcst t := match isBigZcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigZ_to_N t := match t with | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:0%N - | BigZ.one => constr:1%N - | BigZ.two => constr:2%N - | _ => constr:NotConstant + | BigZ.zero => constr:(0%N) + | BigZ.one => constr:(1%N) + | BigZ.two => constr:(2%N) + | _ => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e0c..ec1017f505 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index fe38ea4f2d..850afe5345 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -104,18 +104,18 @@ Ltac isBigQcst t := | BigQ.Qz ?t => isBigZcst t | BigQ.Qq ?n ?d => match isBigZcst n with | true => isBigNcst d - | false => constr:false + | false => constr:(false) end - | BigQ.zero => constr:true - | BigQ.one => constr:true - | BigQ.minus_one => constr:true - | _ => constr:false + | BigQ.zero => constr:(true) + | BigQ.one => constr:(true) + | BigQ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigQcst t := match isBigQcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Add Field BigQfield : BigQfieldth -- cgit v1.2.3