From: Ferruccio Guidi Date: Thu, 16 Nov 2006 15:12:17 +0000 (+0000) Subject: - transcript: patched to generate CoRN_notation.ma instead of CoRN.ma X-Git-Tag: 0.4.95@7852~802 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94873bb61a663b4fca3dc6d07b7bb9f42122003e;p=helm.git - transcript: patched to generate CoRN_notation.ma instead of CoRN.ma - CoRN-Decl: regenerated --- 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 "{