From 94873bb61a663b4fca3dc6d07b7bb9f42122003e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Nov 2006 15:12:17 +0000 Subject: [PATCH] - transcript: patched to generate CoRN_notation.ma instead of CoRN.ma - CoRN-Decl: regenerated --- components/binaries/transcript/Makefile | 12 +- components/binaries/transcript/engine.ml | 11 +- matita/contribs/CoRN-Decl/CoRN.ma | 625 ------------------ matita/contribs/CoRN-Decl/algebra/Basics.ma | 2 +- .../contribs/CoRN-Decl/algebra/CAbGroups.ma | 2 +- .../contribs/CoRN-Decl/algebra/CAbMonoids.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CFields.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CGroups.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CLogic.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CMonoids.ma | 2 +- matita/contribs/CoRN-Decl/algebra/COrdAbs.ma | 2 +- .../contribs/CoRN-Decl/algebra/COrdCauchy.ma | 2 +- .../contribs/CoRN-Decl/algebra/COrdFields.ma | 2 +- .../contribs/CoRN-Decl/algebra/COrdFields2.ma | 2 +- .../CoRN-Decl/algebra/CPoly_ApZero.ma | 2 +- .../CoRN-Decl/algebra/CPoly_Degree.ma | 2 +- .../CoRN-Decl/algebra/CPoly_NthCoeff.ma | 2 +- .../CoRN-Decl/algebra/CPolynomials.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CRings.ma | 2 +- .../contribs/CoRN-Decl/algebra/CSemiGroups.ma | 2 +- .../contribs/CoRN-Decl/algebra/CSetoidFun.ma | 2 +- .../contribs/CoRN-Decl/algebra/CSetoidInc.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CSetoids.ma | 2 +- matita/contribs/CoRN-Decl/algebra/CSums.ma | 2 +- .../CoRN-Decl/algebra/CVectorSpace.ma | 2 +- .../contribs/CoRN-Decl/algebra/Cauchy_COF.ma | 2 +- matita/contribs/CoRN-Decl/algebra/Expon.ma | 2 +- matita/contribs/CoRN-Decl/algebra/ListType.ma | 2 +- matita/contribs/CoRN-Decl/complex/AbsCC.ma | 2 +- matita/contribs/CoRN-Decl/complex/CComplex.ma | 2 +- .../CoRN-Decl/complex/Complex_Exponential.ma | 2 +- matita/contribs/CoRN-Decl/complex/NRootCC.ma | 2 +- .../contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma | 2 +- .../CoRN-Decl/devel/loeb/per/csetfun.ma | 2 +- .../CoRN-Decl/devel/loeb/per/lst2fun.ma | 2 +- matita/contribs/CoRN-Decl/fta/CC_Props.ma | 2 +- .../contribs/CoRN-Decl/fta/CPoly_Contin1.ma | 2 +- matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma | 2 +- matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma | 2 +- matita/contribs/CoRN-Decl/fta/FTA.ma | 2 +- matita/contribs/CoRN-Decl/fta/FTAreg.ma | 2 +- matita/contribs/CoRN-Decl/fta/KeyLemma.ma | 2 +- matita/contribs/CoRN-Decl/fta/KneserLemma.ma | 2 +- matita/contribs/CoRN-Decl/fta/MainLemma.ma | 2 +- matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma | 2 +- .../CoRN-Decl/ftc/CalculusTheorems.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Composition.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Continuity.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Derivative.ma | 2 +- .../contribs/CoRN-Decl/ftc/DerivativeOps.ma | 2 +- .../CoRN-Decl/ftc/Differentiability.ma | 2 +- matita/contribs/CoRN-Decl/ftc/FTC.ma | 2 +- .../contribs/CoRN-Decl/ftc/FunctSequence.ma | 2 +- matita/contribs/CoRN-Decl/ftc/FunctSeries.ma | 2 +- matita/contribs/CoRN-Decl/ftc/FunctSums.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Integral.ma | 2 +- .../contribs/CoRN-Decl/ftc/IntervalFunct.ma | 2 +- .../contribs/CoRN-Decl/ftc/MoreFunSeries.ma | 2 +- .../contribs/CoRN-Decl/ftc/MoreFunctions.ma | 2 +- .../contribs/CoRN-Decl/ftc/MoreIntegrals.ma | 2 +- .../contribs/CoRN-Decl/ftc/MoreIntervals.ma | 2 +- .../contribs/CoRN-Decl/ftc/NthDerivative.ma | 2 +- .../contribs/CoRN-Decl/ftc/PartFunEquality.ma | 2 +- matita/contribs/CoRN-Decl/ftc/PartInterval.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Partitions.ma | 2 +- matita/contribs/CoRN-Decl/ftc/RefLemma.ma | 2 +- matita/contribs/CoRN-Decl/ftc/RefSepRef.ma | 2 +- matita/contribs/CoRN-Decl/ftc/RefSeparated.ma | 2 +- .../contribs/CoRN-Decl/ftc/RefSeparating.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Rolle.ma | 2 +- matita/contribs/CoRN-Decl/ftc/StrongIVT.ma | 2 +- matita/contribs/CoRN-Decl/ftc/Taylor.ma | 2 +- matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma | 2 +- matita/contribs/CoRN-Decl/ftc/WeakIVT.ma | 2 +- .../CoRN-Decl/metrics/CMetricSpaces.ma | 2 +- .../contribs/CoRN-Decl/metrics/CPMSTheory.ma | 2 +- .../CoRN-Decl/metrics/CPseudoMSpaces.ma | 2 +- .../CoRN-Decl/metrics/ContFunctions.ma | 2 +- matita/contribs/CoRN-Decl/metrics/Equiv.ma | 2 +- .../contribs/CoRN-Decl/metrics/IR_CPMSpace.ma | 2 +- matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma | 2 +- .../CoRN-Decl/model/abgroups/QSposabgroup.ma | 2 +- .../CoRN-Decl/model/abgroups/Qabgroup.ma | 2 +- .../CoRN-Decl/model/abgroups/Qposabgroup.ma | 2 +- .../CoRN-Decl/model/abgroups/Zabgroup.ma | 2 +- .../contribs/CoRN-Decl/model/fields/Qfield.ma | 2 +- .../CoRN-Decl/model/groups/QSposgroup.ma | 2 +- .../contribs/CoRN-Decl/model/groups/Qgroup.ma | 2 +- .../CoRN-Decl/model/groups/Qposgroup.ma | 2 +- .../contribs/CoRN-Decl/model/groups/Zgroup.ma | 2 +- .../CoRN-Decl/model/monoids/Nmonoid.ma | 2 +- .../CoRN-Decl/model/monoids/Nposmonoid.ma | 2 +- .../CoRN-Decl/model/monoids/QSposmonoid.ma | 2 +- .../CoRN-Decl/model/monoids/Qmonoid.ma | 2 +- .../CoRN-Decl/model/monoids/Qposmonoid.ma | 2 +- .../CoRN-Decl/model/monoids/Zmonoid.ma | 2 +- .../model/non_examples/N_no_group.ma | 2 +- .../model/non_examples/Npos_no_group.ma | 2 +- .../model/non_examples/Npos_no_monoid.ma | 2 +- .../CoRN-Decl/model/ordfields/Qordfield.ma | 2 +- .../CoRN-Decl/model/reals/Cauchy_IR.ma | 2 +- .../contribs/CoRN-Decl/model/rings/Qring.ma | 2 +- .../contribs/CoRN-Decl/model/rings/Zring.ma | 2 +- .../model/semigroups/Npossemigroup.ma | 2 +- .../CoRN-Decl/model/semigroups/Nsemigroup.ma | 2 +- .../model/semigroups/QSpossemigroup.ma | 2 +- .../model/semigroups/Qpossemigroup.ma | 2 +- .../CoRN-Decl/model/semigroups/Qsemigroup.ma | 2 +- .../CoRN-Decl/model/semigroups/Zsemigroup.ma | 2 +- .../CoRN-Decl/model/setoids/Npossetoid.ma | 2 +- .../CoRN-Decl/model/setoids/Nsetoid.ma | 2 +- .../CoRN-Decl/model/setoids/Qpossetoid.ma | 2 +- .../CoRN-Decl/model/setoids/Qsetoid.ma | 2 +- .../CoRN-Decl/model/setoids/Zsetoid.ma | 2 +- .../CoRN-Decl/model/structures/Npossec.ma | 2 +- .../CoRN-Decl/model/structures/Nsec.ma | 2 +- .../CoRN-Decl/model/structures/Qpossec.ma | 2 +- .../CoRN-Decl/model/structures/Qsec.ma | 2 +- .../CoRN-Decl/model/structures/Zsec.ma | 2 +- .../contribs/CoRN-Decl/reals/Bridges_LUB.ma | 2 +- .../contribs/CoRN-Decl/reals/Bridges_iso.ma | 2 +- .../contribs/CoRN-Decl/reals/CMetricFields.ma | 2 +- .../contribs/CoRN-Decl/reals/CPoly_Contin.ma | 2 +- matita/contribs/CoRN-Decl/reals/CReals.ma | 2 +- matita/contribs/CoRN-Decl/reals/CReals1.ma | 2 +- matita/contribs/CoRN-Decl/reals/CSumsReals.ma | 2 +- matita/contribs/CoRN-Decl/reals/CauchySeq.ma | 2 +- .../contribs/CoRN-Decl/reals/Cauchy_CReals.ma | 2 +- matita/contribs/CoRN-Decl/reals/IVT.ma | 2 +- matita/contribs/CoRN-Decl/reals/Intervals.ma | 2 +- matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma | 2 +- matita/contribs/CoRN-Decl/reals/NRootIR.ma | 2 +- .../contribs/CoRN-Decl/reals/OddPolyRootIR.ma | 2 +- matita/contribs/CoRN-Decl/reals/Q_dense.ma | 2 +- .../contribs/CoRN-Decl/reals/Q_in_CReals.ma | 2 +- matita/contribs/CoRN-Decl/reals/R_morphism.ma | 2 +- matita/contribs/CoRN-Decl/reals/RealFuncts.ma | 2 +- matita/contribs/CoRN-Decl/reals/RealLists.ma | 2 +- matita/contribs/CoRN-Decl/reals/Series.ma | 2 +- matita/contribs/CoRN-Decl/reals/iso_CReals.ma | 2 +- .../CoRN-Decl/tactics/AlgReflection.ma | 2 +- .../CoRN-Decl/tactics/DiffTactics1.ma | 2 +- .../CoRN-Decl/tactics/DiffTactics2.ma | 2 +- .../CoRN-Decl/tactics/DiffTactics3.ma | 2 +- .../CoRN-Decl/tactics/FieldReflection.ma | 2 +- .../CoRN-Decl/tactics/GroupReflection.ma | 2 +- .../CoRN-Decl/tactics/Opaque_algebra.ma | 2 +- .../CoRN-Decl/tactics/RingReflection.ma | 2 +- matita/contribs/CoRN-Decl/tactics/Step.ma | 2 +- .../CoRN-Decl/tactics/Transparent_algebra.ma | 2 +- .../contribs/CoRN-Decl/transc/Exponential.ma | 2 +- .../contribs/CoRN-Decl/transc/InvTrigonom.ma | 2 +- matita/contribs/CoRN-Decl/transc/Pi.ma | 2 +- .../contribs/CoRN-Decl/transc/PowerSeries.ma | 2 +- .../contribs/CoRN-Decl/transc/RealPowers.ma | 2 +- matita/contribs/CoRN-Decl/transc/SinCos.ma | 2 +- .../contribs/CoRN-Decl/transc/TaylorSeries.ma | 2 +- matita/contribs/CoRN-Decl/transc/TrigMon.ma | 2 +- .../CoRN-Decl/transc/Trigonometric.ma | 2 +- 159 files changed, 168 insertions(+), 792 deletions(-) delete mode 100644 matita/contribs/CoRN-Decl/CoRN.ma diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile index 21dedfc0d..7d6cd364f 100644 --- a/components/binaries/transcript/Makefile +++ b/components/binaries/transcript/Makefile @@ -28,13 +28,13 @@ all: transcript .depend @echo -n opt: transcript.opt $(EXTRAS) .depend.opt - #echo -n + @echo -n -transcript: $(CMIS) $(CMOS) $(EXTRAS) $(LIBRARIES) +transcript: $(CMIS) $(CMOS) $(EXTRAS) @echo " OCAMLC $(CMOS)" $(H)$(OCAMLC) -o $@ $(CMOS) -transcript.opt: $(CMIS) $(CMXS) $(EXTRAS) $(LIBRARIES_OPT) +transcript.opt: $(CMIS) $(CMXS) $(EXTRAS) @echo " OCAMLOPT $(CMXS)" $(H)$(OCAMLOPT) -o $@ $(CMXS) @@ -67,13 +67,13 @@ depend: .depend depend.opt: .depend.opt -%.cmi: %.mli $(EXTRAS) +%.cmi: %.mli $(EXTRAS) @echo " OCAMLC $<" $(H)$(OCAMLC) -c $< -%.cmo %.cmi: %.ml $(EXTRAS) +%.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES) @echo " OCAMLC $<" $(H)$(OCAMLC) -c $< -%.cmx: %.ml $(EXTRAS) +%.cmx: %.ml $(EXTRAS) $(LIBRARIES_OPT) @echo " OCAMLOPT $<" $(H)$(OCAMLOPT) -c $< %.ml %.mli: %.mly $(EXTRAS) diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml index 8908897dd..62fcf03df 100644 --- a/components/binaries/transcript/engine.ml +++ b/components/binaries/transcript/engine.ml @@ -131,8 +131,8 @@ let set_baseuri st name = let baseuri = Filename.concat st.output_base_uri name in set_items st name [T.BaseUri baseuri] -let require st name = - set_items st name [T.Include st.package] +let require st name inc = + set_items st name [T.Include inc] let commit st name = let i = get_index st name in @@ -147,6 +147,7 @@ let commit st name = st.scripts.(i) <- default_script let produce st = + let notation = st.package ^ "_notation" in let init name = set_heading st name; set_baseuri st name in let partition = function | T.Notation _ -> false @@ -180,10 +181,10 @@ let produce st = let local_items, global_items = List.partition partition items in let comment = T.Line (Printf.sprintf "From %s" name) in if global_items <> [] then - set_items st st.package (comment :: global_items); - init name; require st name; + set_items st notation (comment :: global_items); + init name; require st name notation; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in - init st.package; List.iter (produce st) st.files; commit st st.package + init notation; List.iter (produce st) st.files; commit st notation diff --git a/matita/contribs/CoRN-Decl/CoRN.ma b/matita/contribs/CoRN-Decl/CoRN.ma deleted file mode 100644 index fe83e449b..000000000 --- a/matita/contribs/CoRN-Decl/CoRN.ma +++ /dev/null @@ -1,625 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/CoRN-Decl/CoRN". - -(* From algebra/Basics ****************************************************) - -(* NOTATION -Notation Pair := (pair (B:=_)). -*) - -(* NOTATION -Notation Proj1 := (proj1 (B:=_)). -*) - -(* NOTATION -Notation Proj2 := (proj2 (B:=_)). -*) - -(* From algebra/CFields ***************************************************) - -(* NOTATION -Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80). -*) - -(* NOTATION -Notation "{1/} x" := (Frecip x) (at level 2, right associativity). -*) - -(* NOTATION -Infix "{/}" := Fdiv (at level 41, no associativity). -*) - -(* From algebra/CGroups ***************************************************) - -(* NOTATION -Notation "[--] x" := (cg_inv x) (at level 2, right associativity). -*) - -(* NOTATION -Infix "[-]" := cg_minus (at level 50, left associativity). -*) - -(* NOTATION -Notation "{--} x" := (Finv x) (at level 2, right associativity). -*) - -(* NOTATION -Infix "{-}" := Fminus (at level 50, left associativity). -*) - -(* From algebra/CLogic ****************************************************) - -(* NOTATION -Infix "IFF" := Iff (at level 60, right associativity). -*) - -(* NOTATION -Infix "or" := COr (at level 85, right associativity). -*) - -(* NOTATION -Infix "and" := CAnd (at level 80, right associativity). -*) - -(* NOTATION -Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp) - (at level 0, x at level 99) : type_scope. -*) - -(* NOTATION -Notation "{ x : A | P | Q }" := - (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) : - type_scope. -*) - -(* NOTATION -Notation ProjT1 := (proj1_sigT _ _). -*) - -(* NOTATION -Notation ProjT2 := (proj2_sigT _ _). -*) - -(* From algebra/CMonoids **************************************************) - -(* NOTATION -Notation Zero := (cm_unit _). -*) - -(* From algebra/COrdAbs ***************************************************) - -(* NOTATION -Notation ZeroR := (Zero:R). -*) - -(* NOTATION -Notation AbsBig := (absBig _). -*) - -(* From algebra/COrdFields ************************************************) - -(* NOTATION -Infix "[<]" := cof_less (at level 70, no associativity). -*) - -(* NOTATION -Infix "[>]" := greater (at level 70, no associativity). -*) - -(* NOTATION -Infix "[<=]" := leEq (at level 70, no associativity). -*) - -(* NOTATION -Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). -*) - -(* NOTATION -Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). -*) - -(* From algebra/COrdFields2 ***********************************************) - -(* NOTATION -Notation ZeroR := (Zero:R). -*) - -(* NOTATION -Notation OneR := (One:R). -*) - -(* From algebra/CPoly_ApZero **********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* From algebra/CPoly_Degree **********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation FX := (cpoly_cring F). -*) - -(* From algebra/CPoly_NthCoeff ********************************************) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* From algebra/CPolynomials **********************************************) - -(* NOTATION -Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity). -*) - -(* NOTATION -Notation RX := (cpoly_cring CR). -*) - -(* NOTATION -Infix "!" := cpoly_apply_fun (at level 1, no associativity). -*) - -(* NOTATION -Notation RX := (cpoly_cring R). -*) - -(* NOTATION -Notation Cpoly := (cpoly CR). -*) - -(* NOTATION -Notation Cpoly_zero := (cpoly_zero CR). -*) - -(* NOTATION -Notation Cpoly_linear := (cpoly_linear CR). -*) - -(* NOTATION -Notation Cpoly_cring := (cpoly_cring CR). -*) - -(* From algebra/CRings ****************************************************) - -(* NOTATION -Notation One := (cr_one _). -*) - -(* NOTATION -Infix "[*]" := cr_mult (at level 40, left associativity). -*) - -(* NOTATION -Notation "x [^] n" := (nexp_op _ n x) (at level 20). -*) - -(* NOTATION -Notation Two := (nring 2). -*) - -(* NOTATION -Notation Three := (nring 3). -*) - -(* NOTATION -Notation Four := (nring 4). -*) - -(* NOTATION -Notation Six := (nring 6). -*) - -(* NOTATION -Notation Eight := (nring 8). -*) - -(* NOTATION -Notation Twelve := (nring 12). -*) - -(* NOTATION -Notation Sixteen := (nring 16). -*) - -(* NOTATION -Notation Nine := (nring 9). -*) - -(* NOTATION -Notation Eighteen := (nring 18). -*) - -(* NOTATION -Notation TwentyFour := (nring 24). -*) - -(* NOTATION -Notation FortyEight := (nring 48). -*) - -(* NOTATION -Infix "{*}" := Fmult (at level 40, left associativity). -*) - -(* NOTATION -Infix "{**}" := Fscalmult (at level 40, left associativity). -*) - -(* NOTATION -Infix "{^}" := Fnth (at level 30, right associativity). -*) - -(* From algebra/CSemiGroups ***********************************************) - -(* NOTATION -Infix "[+]" := csg_op (at level 50, left associativity). -*) - -(* NOTATION -Infix "{+}" := Fplus (at level 50, left associativity). -*) - -(* From algebra/CSetoidFun ************************************************) - -(* NOTATION -Notation Conj := (conjP _). -*) - -(* NOTATION -Notation BDom := (bpfdom _ _). -*) - -(* NOTATION -Notation Dom := (pfdom _). -*) - -(* NOTATION -Notation Part := (pfpfun _). -*) - -(* NOTATION -Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). -*) - -(* NOTATION -Notation FId := (Fid _). -*) - -(* NOTATION -Infix "[o]" := Fcomp (at level 65, no associativity). -*) - -(* NOTATION -Notation Prj1 := (prj1 _ _ _ _). -*) - -(* NOTATION -Notation Prj2 := (prj2 _ _ _ _). -*) - -(* From algebra/CSetoids **************************************************) - -(* NOTATION -Infix "[=]" := cs_eq (at level 70, no associativity). -*) - -(* NOTATION -Infix "[#]" := cs_ap (at level 70, no associativity). -*) - -(* NOTATION -Infix "[~=]" := cs_neq (at level 70, no associativity). -*) - -(* From algebra/CVectorSpace **********************************************) - -(* NOTATION -Infix "[']" := vs_op (at level 30, no associativity). -*) - -(* From algebra/Expon *****************************************************) - -(* NOTATION -Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0). -*) - -(* From complex/CComplex **************************************************) - -(* NOTATION -Notation CCX := (cpoly_cring CC). -*) - -(* NOTATION -Infix "[+I*]" := cc_set_CC (at level 48, no associativity). -*) - -(* From ftc/FTC ***********************************************************) - -(* NOTATION -Notation "[-S-] F" := (Fprim F) (at level 20). -*) - -(* From ftc/Integral ******************************************************) - -(* NOTATION -Notation Integral := (integral _ _ Hab). -*) - -(* From ftc/RefLemma ******************************************************) - -(* NOTATION -Notation g := RL_g. -*) - -(* NOTATION -Notation h := RL_h. -*) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)). -*) - -(* NOTATION -Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)). -*) - -(* NOTATION -Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)). -*) - -(* From ftc/RefSeparated **************************************************) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). -*) - -(* NOTATION -Notation just2 := - (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)). -*) - -(* From ftc/RefSeparating *************************************************) - -(* NOTATION -Notation m := RS'_m. -*) - -(* NOTATION -Notation h := RS'_h. -*) - -(* NOTATION -Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)). -*) - -(* NOTATION -Notation just2 := - (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)). -*) - -(* From ftc/Rolle *********************************************************) - -(* NOTATION -Notation cp := (compact_part a b Hab' d Hd). -*) - -(* From ftc/TaylorLemma ***************************************************) - -(* NOTATION -Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a). -*) - -(* NOTATION -Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b). -*) - -(* From ftc/WeakIVT *******************************************************) - -(* NOTATION -Infix "**" := prodT (at level 20). -*) - -(* From metrics/CPseudoMSpaces ********************************************) - -(* NOTATION -Infix "[-d]" := cms_d (at level 68, left associativity). -*) - -(* From model/structures/Nsec *********************************************) - -(* NOTATION -Infix "{#N}" := ap_nat (no associativity, at level 90). -*) - -(* From model/structures/Qsec *********************************************) - -(* NOTATION -Infix "{=Q}" := Qeq (no associativity, at level 90). -*) - -(* NOTATION -Infix "{#Q}" := Qap (no associativity, at level 90). -*) - -(* NOTATION -Infix "{