diff options
| -rw-r--r-- | .depend.coq | 27 | ||||
| -rw-r--r-- | .depend.newcoq | 29 | ||||
| -rw-r--r-- | Makefile | 5 | ||||
| -rwxr-xr-x | theories/Init/Logic.v | 51 | ||||
| -rw-r--r-- | theories/Init/LogicSyntax.v | 66 | ||||
| -rwxr-xr-x | theories/Init/Logic_Type.v | 53 | ||||
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 51 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 3 | ||||
| -rwxr-xr-x | theories/Init/Prelude.v | 2 | ||||
| -rwxr-xr-x | theories/Init/Specif.v | 24 | ||||
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 38 | ||||
| -rwxr-xr-x | theories/Init/Wf.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Raxioms.v | 1 | ||||
| -rw-r--r-- | theories/Reals/Rbase.v | 1 | ||||
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 1 | ||||
| -rw-r--r-- | theories/Reals/TypeSyntax.v | 15 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
17 files changed, 130 insertions, 245 deletions
diff --git a/.depend.coq b/.depend.coq index ab0164b7a..f24c76f70 100644 --- a/.depend.coq +++ b/.depend.coq @@ -1,10 +1,9 @@ -theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v -theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo +theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo -theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo +theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo -theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo @@ -55,15 +54,12 @@ theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/Newto theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Init/Notations.vo: theories/Init/Notations.v theories/Init/Datatypes.vo: theories/Init/Datatypes.v theories/Init/Notations.vo -theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo +theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Notations.vo theories/Init/Datatypes.vo -theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo -theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Notations.vo theories/Init/Logic.vo -theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Specif.vo -theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo -theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo -theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Notations.vo theories/Init/Logic_Type.vo -theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo +theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo +theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Notations.vo theories/Init/Logic.vo +theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/Datatypes.vo +theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Logic.vo theories/Init/Specif.vo theories/Init/Peano.vo theories/Init/Wf.vo theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/Hurkens.vo theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo @@ -182,13 +178,12 @@ theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/R theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theories/Logic/Eqdep.vo theories/Wellfounded/Lexicographic_Product.vo: theories/Wellfounded/Lexicographic_Product.v theories/Logic/Eqdep.vo theories/Relations/Relation_Operators.vo theories/Wellfounded/Transitive_Closure.vo -theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v -theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo +theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo -theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo +theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo -theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo diff --git a/.depend.newcoq b/.depend.newcoq index 64090f966..455ce85ce 100644 --- a/.depend.newcoq +++ b/.depend.newcoq @@ -1,10 +1,9 @@ -newtheories/Reals/TypeSyntax.vo: newtheories/Reals/TypeSyntax.v -newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/TypeSyntax.vo +newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo: newtheories/Reals/Rsyntax.v newtheories/Reals/Rdefinitions.vo -newtheories/Reals/Raxioms.vo: newtheories/Reals/Raxioms.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo newtheories/Reals/TypeSyntax.vo +newtheories/Reals/Raxioms.vo: newtheories/Reals/Raxioms.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo newtheories/Reals/RIneq.vo: newtheories/Reals/RIneq.v newtheories/Reals/Raxioms.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newcontrib/field/Field.vo newtheories/Reals/DiscrR.vo: newtheories/Reals/DiscrR.v newtheories/Reals/RIneq.vo newcontrib/omega/Omega.vo -newtheories/Reals/Rbase.vo: newtheories/Reals/Rbase.v newtheories/Reals/Rdefinitions.vo newtheories/Reals/TypeSyntax.vo newtheories/Reals/Raxioms.vo newtheories/Reals/RIneq.vo newtheories/Reals/DiscrR.vo +newtheories/Reals/Rbase.vo: newtheories/Reals/Rbase.v newtheories/Reals/Rdefinitions.vo newtheories/Reals/Raxioms.vo newtheories/Reals/RIneq.vo newtheories/Reals/DiscrR.vo newtheories/Reals/R_Ifp.vo: newtheories/Reals/R_Ifp.v newtheories/Reals/Rbase.vo newcontrib/omega/Omega.vo newtheories/Reals/Rbasic_fun.vo: newtheories/Reals/Rbasic_fun.v newtheories/Reals/Rbase.vo newtheories/Reals/R_Ifp.vo newcontrib/fourier/Fourier.vo newtheories/Reals/R_sqr.vo: newtheories/Reals/R_sqr.v newtheories/Reals/Rbase.vo newtheories/Reals/Rbasic_fun.vo @@ -55,15 +54,12 @@ newtheories/Reals/Integration.vo: newtheories/Reals/Integration.v newtheories/Re newtheories/Reals/Reals.vo: newtheories/Reals/Reals.v newtheories/Reals/Rbase.vo newtheories/Reals/Rfunctions.vo newtheories/Reals/SeqSeries.vo newtheories/Reals/Rtrigo.vo newtheories/Reals/Ranalysis.vo newtheories/Reals/Integration.vo newtheories/Init/Notations.vo: newtheories/Init/Notations.v newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v newtheories/Init/Notations.vo -newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Datatypes.vo +newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo -newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo -newtheories/Init/LogicSyntax.vo: newtheories/Init/LogicSyntax.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo -newtheories/Init/SpecifSyntax.vo: newtheories/Init/SpecifSyntax.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Specif.vo -newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo -newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Datatypes.vo -newtheories/Init/Logic_TypeSyntax.vo: newtheories/Init/Logic_TypeSyntax.v newtheories/Init/Notations.vo newtheories/Init/Logic_Type.vo -newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/LogicSyntax.vo newtheories/Init/Specif.vo newtheories/Init/SpecifSyntax.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo +newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo +newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo +newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Datatypes.vo +newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Specif.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo newtheories/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v newtheories/Logic/ProofIrrelevance.vo: newtheories/Logic/ProofIrrelevance.v newtheories/Logic/Hurkens.vo newtheories/Logic/Classical.vo: newtheories/Logic/Classical.v newtheories/Logic/Classical_Prop.vo newtheories/Logic/Classical_Pred_Set.vo @@ -116,7 +112,7 @@ newtheories/ZArith/zarith_aux.vo: newtheories/ZArith/zarith_aux.v newtheories/Ar newtheories/ZArith/Zhints.vo: newtheories/ZArith/Zhints.v newtheories/ZArith/zarith_aux.vo newtheories/ZArith/auxiliary.vo newtheories/ZArith/Zsyntax.vo newtheories/ZArith/Zmisc.vo newtheories/ZArith/Wf_Z.vo newtheories/ZArith/Zlogarithm.vo: newtheories/ZArith/Zlogarithm.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo newtheories/ZArith/Zpower.vo newtheories/ZArith/Zpower.vo: newtheories/ZArith/Zpower.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zcomplements.vo -newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo newtheories/Lists/PolyList.vo +newtheories/ZArith/Zcomplements.vo: newtheories/ZArith/Zcomplements.v newcontrib/ring/ZArithRing.vo newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newtheories/Arith/Wf_nat.vo newtheories/Lists/PolyList.vo newtheories/ZArith/Zdiv.vo: newtheories/ZArith/Zdiv.v newtheories/ZArith/ZArith_base.vo newcontrib/omega/Omega.vo newcontrib/ring/ZArithRing.vo newtheories/ZArith/Zcomplements.vo newtheories/ZArith/Zsqrt.vo: newtheories/ZArith/Zsqrt.v newtheories/ZArith/ZArith_base.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newtheories/ZArith/Zwf.vo: newtheories/ZArith/Zwf.v newtheories/ZArith/ZArith_base.vo newtheories/Arith/Wf_nat.vo newcontrib/omega/Omega.vo @@ -182,13 +178,12 @@ newtheories/Wellfounded/Union.vo: newtheories/Wellfounded/Union.v newtheories/Re newtheories/Wellfounded/Wellfounded.vo: newtheories/Wellfounded/Wellfounded.v newtheories/Wellfounded/Disjoint_Union.vo newtheories/Wellfounded/Inclusion.vo newtheories/Wellfounded/Inverse_Image.vo newtheories/Wellfounded/Lexicographic_Exponentiation.vo newtheories/Wellfounded/Lexicographic_Product.vo newtheories/Wellfounded/Transitive_Closure.vo newtheories/Wellfounded/Union.vo newtheories/Wellfounded/Well_Ordering.vo newtheories/Wellfounded/Well_Ordering.vo: newtheories/Wellfounded/Well_Ordering.v newtheories/Logic/Eqdep.vo newtheories/Wellfounded/Lexicographic_Product.vo: newtheories/Wellfounded/Lexicographic_Product.v newtheories/Logic/Eqdep.vo newtheories/Relations/Relation_Operators.vo newtheories/Wellfounded/Transitive_Closure.vo -newtheories/Reals/TypeSyntax.vo: newtheories/Reals/TypeSyntax.v -newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/TypeSyntax.vo +newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo: newtheories/Reals/Rsyntax.v newtheories/Reals/Rdefinitions.vo -newtheories/Reals/Raxioms.vo: newtheories/Reals/Raxioms.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo newtheories/Reals/TypeSyntax.vo +newtheories/Reals/Raxioms.vo: newtheories/Reals/Raxioms.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/Rsyntax.vo newtheories/Reals/RIneq.vo: newtheories/Reals/RIneq.v newtheories/Reals/Raxioms.vo newcontrib/ring/ZArithRing.vo newcontrib/omega/Omega.vo newcontrib/field/Field.vo newtheories/Reals/DiscrR.vo: newtheories/Reals/DiscrR.v newtheories/Reals/RIneq.vo newcontrib/omega/Omega.vo -newtheories/Reals/Rbase.vo: newtheories/Reals/Rbase.v newtheories/Reals/Rdefinitions.vo newtheories/Reals/TypeSyntax.vo newtheories/Reals/Raxioms.vo newtheories/Reals/RIneq.vo newtheories/Reals/DiscrR.vo +newtheories/Reals/Rbase.vo: newtheories/Reals/Rbase.v newtheories/Reals/Rdefinitions.vo newtheories/Reals/Raxioms.vo newtheories/Reals/RIneq.vo newtheories/Reals/DiscrR.vo newtheories/Reals/R_Ifp.vo: newtheories/Reals/R_Ifp.v newtheories/Reals/Rbase.vo newcontrib/omega/Omega.vo newtheories/Reals/Rbasic_fun.vo: newtheories/Reals/Rbasic_fun.v newtheories/Reals/Rbase.vo newtheories/Reals/R_Ifp.vo newcontrib/fourier/Fourier.vo newtheories/Reals/R_sqr.vo: newtheories/Reals/R_sqr.v newtheories/Reals/Rbase.vo newtheories/Reals/Rbasic_fun.vo @@ -528,9 +528,8 @@ states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) INITVO=theories/Init/Notations.vo \ theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic.vo theories/Init/Specif.vo \ - theories/Init/LogicSyntax.vo theories/Init/SpecifSyntax.vo \ theories/Init/Logic_Type.vo theories/Init/Wf.vo \ - theories/Init/Logic_TypeSyntax.vo theories/Init/Prelude.vo + theories/Init/Prelude.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) @@ -635,7 +634,7 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \ theories/Wellfounded/Well_Ordering.vo \ theories/Wellfounded/Lexicographic_Product.vo -REALSBASEVO=theories/Reals/TypeSyntax.vo \ +REALSBASEVO=\ theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \ theories/Reals/Raxioms.vo theories/Reals/RIneq.vo \ theories/Reals/DiscrR.vo theories/Reals/Rbase.vo \ diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 91ec84c42..c24b86426 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -95,7 +95,7 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (at level 1, c1, c2, c3 at level 8) V8only (at level 200). -Section First_order_quantifiers. +(** First-order quantifiers *) (** [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an [x] of type [A] which satisfies the predicate [P] ([A] is of type @@ -110,15 +110,41 @@ Section First_order_quantifiers. construction [(all A P)], or simply [(All P)], is provided as an abbreviation of [(x:A)(P x)] *) - Inductive ex [A:Type;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex A P). +Inductive ex [A:Type;P:A->Prop] : Prop + := ex_intro : (x:A)(P x)->(ex A P). - Inductive ex2 [A:Type;P,Q:A->Prop] : Prop - := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q). +Inductive ex2 [A:Type;P,Q:A->Prop] : Prop + := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q). - Definition all := [A:Type][P:A->Prop](x:A)(P x). +Definition all := [A:Type][P:A->Prop](x:A)(P x). - Section universal_quantification. +(*Rule order is important to give printing priority to fully typed ALL and EX*) + +V7only [ Notation Ex := (ex ?). ]. +Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x ident, p at level 80). +Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x ident, p at level 80). + +V7only [ Notation Ex2 := (ex2 ?). ]. +Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) + (at level 10, p, q at level 8) + V8only "'EX2' x | p & q" (at level 200, x ident, p, q at level 80). +Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) + (at level 10, p, q at level 8) + V8only "'EX2' x : t | p & q" + (at level 200, x ident, t at level 200, p, q at level 80). + +V7only [Notation All := (all ?).]. +Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x ident, p at level 200). +Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x ident, t, p at level 200). + + +(** Universal quantification *) + +Section universal_quantification. Variable A : Type. Variable P : A->Prop. @@ -135,7 +161,7 @@ Section First_order_quantifiers. End universal_quantification. -End First_order_quantifiers. +(** Equality *) (** [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality of [x] and [y]. Both [x] and [y] must belong to the same type [A]. @@ -249,3 +275,12 @@ Proof. Qed. Hints Immediate sym_eq sym_not_eq : core v62. + +V7only[ +(** Parsing only of things in [Logic.v] *) +Notation "< A > 'All' ( P )" :=(all A P) (A annot, at level 1, only parsing). +Notation "< A > x = y" := (eq A x y) + (A annot, at level 1, x at level 0, only parsing). +Notation "< A > x <> y" := ~(eq A x y) + (A annot, at level 1, x at level 0, only parsing). +]. diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v deleted file mode 100644 index 53940f237..000000000 --- a/theories/Init/LogicSyntax.v +++ /dev/null @@ -1,66 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Export Notations. -Require Export Logic. - -(** Symbolic notations for things in [Logic.v] *) -(* -V7only[ -Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1). -]. - -Notation "~ x" := (not x) (at level 5, right associativity) - V8only (at level 55, right associativity). -Notation "x = y :> T" := (!eq T x y). -Notation "x = y" := (eq ? x y) (at level 5, no associativity). -Notation "x <> y :> T" := (not (!eq T x y)) (at level 5, y at next level, no associativity). -Notation "x <> y" := (not (eq ? x y)) (at level 5, no associativity). - -Infix RIGHTA 6 "/\\" and. -Infix RIGHTA 7 "\\/" or. -Infix RIGHTA 8 "<->" iff. - -Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) - (at level 1, c1, c2, c3 at level 8) - V8only (at level 200). -*) - -(* Order is important to give printing priority to fully typed ALL and EX *) - -V7only [ Notation All := (all ?). ]. -Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) - V8only (at level 200, p at level 200). -Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) - V8only (at level 200). - -V7only [ Notation Ex := (ex ?). ]. -Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). -Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). - -V7only [ Notation Ex2 := (ex2 ?). ]. -Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8) - V8only "'EX2' x | p & q" (at level 200, x at level 80). -Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) - (at level 10, p, q at level 8) - V8only "'EX2' x : t | p & q" (at level 200, x at level 80). - -V7only[ -(** Parsing only of things in [Logic.v] *) - -Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing). -Notation "< A > x = y" := (eq A x y) - (A annot, at level 1, x at level 0, only parsing). -Notation "< A > x <> y" := ~(eq A x y) - (A annot, at level 1, x at level 0, only parsing). -]. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index e5416276b..2064d585b 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -14,10 +14,10 @@ V7only [Unset Implicit Arguments.]. (** This module defines quantification on the world [Type] ([Logic.v] was defining it on the world [Set]) *) +Require Notations. Require Export Logic. -Require LogicSyntax. - +V7only [ (* (** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)] when [A] is of type [Type] *) @@ -25,11 +25,15 @@ Require LogicSyntax. Definition allT := [A:Type][P:A->Prop](x:A)(P x). *) -V7only [ Notation allT := all (only parsing). Notation inst := Logic.inst (only parsing). Notation gen := Logic.gen (only parsing). -]. + +(* Order is important to give printing priority to fully typed ALL and EX *) + +Notation AllT := (all ?). +Notation "'ALLT' x | p" := (all ? [x]p) (at level 10, p at level 8). +Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8). (* Section universal_quantification. @@ -63,22 +67,28 @@ Inductive exT [A:Type;P:A->Prop] : Prop := exT_intro : (x:A)(P x)->(exT A P). *) -V7only [ Notation exT := ex (only parsing). Notation exT_intro := ex_intro (only parsing). Notation exT_ind := ex_ind (only parsing). -]. + +Notation ExT := (ex ?). +Notation "'EXT' x | p" := (ex ? [x]p) (at level 10, p at level 8). +Notation "'EXT' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8). (* Inductive exT2 [A:Type;P,Q:A->Prop] : Prop := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q). *) -V7only [ Notation exT2 := ex2 (only parsing). Notation exT_intro2 := ex_intro2 (only parsing). Notation exT2_ind := ex2_ind (only parsing). -]. + +Notation ExT2 := (ex2 ?). +Notation "'EXT' x | p & q" := (ex2 ? [x]p [x]q) + (at level 10, p, q at level 8). +Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) + (at level 10, p, q at level 8). (* (** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) @@ -93,13 +103,19 @@ Inductive eqT [A:Type;x:A] : A -> Prop Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62. *) -V7only [ + Notation eqT := eq (only parsing). Notation refl_eqT := refl_equal (only parsing). Notation eqT_ind := eq_ind (only parsing). Notation eqT_rect := eq_rect (only parsing). Notation eqT_rec := eq_rec (only parsing). -]. + +Notation "x == y" := (eq ? x y) (at level 5, no associativity, only parsing). + +(** Parsing only of things in [Logic_type.v] *) + +Notation "< A > x == y" := (eq A x y) + (A annot, at level 1, x at level 0, only parsing). (* Section Equality_is_a_congruence. @@ -131,12 +147,11 @@ Section Equality_is_a_congruence. End Equality_is_a_congruence. *) -V7only [ + Notation sym_eqT := sym_eq (only parsing). Notation trans_eqT := trans_eq (only parsing). Notation congr_eqT := f_equal (only parsing). Notation sym_not_eqT := sym_not_eq (only parsing). -]. (* Hints Immediate sym_eqT sym_not_eqT : core v62. @@ -158,7 +173,6 @@ Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. *) -V7only [ Notation eqT_ind_r := eq_ind_r (only parsing). Notation eqT_rec_r := eq_rec_r (only parsing). Notation eqT_rect_r := eq_rect_r (only parsing). @@ -173,9 +187,18 @@ Definition notT := [A:Type] A->EmptyT. (** Have you an idea of what means [identityT A a b]? No matter! *) -Inductive identityT [A:Type; a:A] : A->Type := +Uninterpreted Notation "x === y :> A" + (at level 5, y at next level, no associativity). + +Inductive identityT [A:Type; a:A] : (b:A)Type as "a === b :> A" := refl_identityT : (identityT A a a). +V7only [ +Notation "< A > x === y" := (!identityT A x y) + (A annot, at level 1, x at level 0, only parsing). +]. +Notation "x === y" := (identityT ? x y) (at level 5, no associativity). + Hints Resolve refl_identityT : core v62. Section IdentityT_is_a_congruence. @@ -254,6 +277,8 @@ Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C := Hints Immediate sym_idT sym_not_idT : core v62. +V7only [ Implicits fstT [1 2]. Implicits sndT [1 2]. Implicits pairT [1 2]. +]. diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v deleted file mode 100644 index e48b15062..000000000 --- a/theories/Init/Logic_TypeSyntax.v +++ /dev/null @@ -1,51 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Notations. -Require Logic_Type. - -(** Symbolic notations for things in [Logic_type.v] *) - -V7only [ -Notation "x == y" := (eq ? x y) (at level 5, no associativity, only parsing). -Notation "x === y" := (identityT ? x y) (at level 5, no associativity). - -(* Order is important to give printing priority to fully typed ALL and EX *) - -Notation AllT := (all ?). -Notation "'ALLT' x | p" := (all ? [x]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). -Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). - -Notation ExT := (ex ?). -Notation "'EXT' x | p" := (ex ? [x]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). -Notation "'EXT' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) - V8only (at level 200, x at level 80). - -Notation ExT2 := (ex2 ?). -Notation "'EXT' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8) - V8only "'EXT2' x | p & q" (at level 200, x at level 80). -Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) - (at level 10, p, q at level 8) - V8only "'EXT2' x : t | p & q" (at level 200, x at level 80). -]. - - -V7only[ -(** Parsing only of things in [Logic_type.v] *) -Notation "< A > x == y" := (eq A x y) - (A annot, at level 1, x at level 0, only parsing). - -Notation "< A > x === y" := (identityT A x y) - (A annot, at level 1, x at level 0, only parsing). -]. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 41f26ffda..077226035 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -24,9 +24,8 @@ Case analysis on [nat] and induction on [nat * nat] are provided too *) Require Notations. -Require Logic. -Require LogicSyntax. Require Datatypes. +Require Logic. Open Local Scope nat_scope. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 972a80986..e7ad28e3f 100755 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -11,8 +11,6 @@ Require Export Notations. Require Export Datatypes. Require Export Logic. -Require Export LogicSyntax. Require Export Specif. -Require Export SpecifSyntax. Require Export Peano. Require Export Wf. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index c9617362d..7a05a89f7 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -13,9 +13,9 @@ V7only [Unset Implicit Arguments.]. (** Basic specifications : Sets containing logical information *) +Require Notations. Require Datatypes. Require Logic. -Require LogicSyntax. (** Subsets *) @@ -100,16 +100,16 @@ Inductive sumbool [A,B:Prop] : Set as "{ A } + { B }" := left : A -> {A}+{B} | right : B -> {A}+{B}. -(* - (** Syntax sumor ["_+{_}"]. *) - Inductive sumor [A:Set;B:Prop] : Set - := inleft : A -> (sumor A B) - | inright : B -> (sumor A B). -*) Inductive sumor [A:Set;B:Prop] : Set as "A + { B }" := inleft : A -> A+{B} | inright : B -> A+{B}. +(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) + +Notation "B + { x : A | P }" := B + (sig A [x:A]P) (only parsing). +Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) (only parsing). +Notation "B + { x : A & P }" := B + (sigS A [x:A]P) (only parsing). +Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) (only parsing). (** Choice *) @@ -161,6 +161,9 @@ Definition error := None. Definition except := False_rec. (* for compatibility with previous versions *) +Notation Except := (except ?). +Notation Error := (error ?). + Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C. Proof. Intros A C h1 h2. @@ -188,3 +191,10 @@ Section projections_sigT. Cases H of (existT x h) => h end. End projections_sigT. + +V7only [ +Notation ProjS1 := (projS1 ? ?). +Notation ProjS2 := (projS2 ? ?). +Notation Value := (value ?). +]. + diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v deleted file mode 100644 index eb9c7cc49..000000000 --- a/theories/Init/SpecifSyntax.v +++ /dev/null @@ -1,38 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Notations. -Require Datatypes. -Require Specif. - -(** Extra factorization of parsing rules *) - -(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) - -Notation "B + { x : A | P }" := B + (sig A [x:A]P) (only parsing). -Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) (only parsing). -Notation "B + { x : A & P }" := B + (sigS A [x:A]P) (only parsing). -Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) (only parsing). - -(** Symbolic notations for definitions in [Specif.v] *) - -(* -Notation "{ A } + { B }" := (sumbool A B). -Notation "A + { B }" := (sumor A B). -*) - -V7only [ -Notation ProjS1 := (projS1 ? ?). -Notation ProjS2 := (projS2 ? ?). -Notation Value := (value ?). -]. - -Notation Except := (except ?). -Notation Error := (error ?). diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 93111571f..fbc71a3ea 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -17,8 +17,8 @@ V7only [Unset Implicit Arguments.]. from a well-founded ordering on a given set *) +Require Notations. Require Logic. -Require LogicSyntax. Require Datatypes. (** Well-founded induction principle on Prop *) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index e90fa2148..4516a206f 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,7 +14,6 @@ Require Export ZArith_base. Require Export Rsyntax. -Require Export TypeSyntax. V7only [Import R_scope.]. Open Local Scope R_scope. V7only [ diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index d0c8e1f30..1df44bbf5 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -9,7 +9,6 @@ (*i $Id$ i*) Require Export Rdefinitions. -Require Export TypeSyntax. Require Export Raxioms. Require Export RIneq. Require Export DiscrR. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 96b682e04..c3f3ba5c9 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -14,7 +14,6 @@ (*********************************************************) Require Export ZArith_base. -Require Export TypeSyntax. Parameter R:Type. diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v deleted file mode 100644 index 4653e6bb8..000000000 --- a/theories/Reals/TypeSyntax.v +++ /dev/null @@ -1,15 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(*********************************************************) -(* Or and Exist in Type *) -(* *) -(*********************************************************) - diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index de9db0a81..0786cc0f8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -553,7 +553,9 @@ let is_obsolete_module (_,qid) = (match string_of_id id with | ("Refine" | "Inv" | "Equality" | "EAuto" | "AutoRewrite" | "EqDecide" | "Xml" | "Extraction" | "Tauto" | "Setoid_replace" - | "Elimdep" ) + | "Elimdep" + | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax" + | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax") -> true | _ -> false) | _ -> false @@ -717,7 +719,7 @@ let vernac_declare_implicits locqid = function let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype (Global.env()) [] [] t in + let t = Detyping.detype (false,Global.env()) [] [] t in List.iter (fun id -> Reserve.declare_reserved_type id t) idl let make_silent_if_not_pcoq b = |