From f620bf94af6c347926ed1c2328462efab7018b21 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 5 Sep 2008 18:37:01 +0000 Subject: [PATCH] transcript: we now check for non-existing objects procedural/Coq: we now generate from ufficial 8.0pl2 that does not have the Num directory --- .../binaries/transcript/.depend.opt | 6 +- .../components/binaries/transcript/engine.ml | 22 +- .../components/binaries/transcript/engine.mli | 2 +- .../components/binaries/transcript/grafite.ml | 21 +- .../components/binaries/transcript/options.ml | 4 + .../components/binaries/transcript/top.ml | 24 +- .../binaries/transcript/v8Parser.mly | 1 + .../contribs/procedural/Coq/Arith/Arith.mma | 18 +- .../contribs/procedural/Coq/Arith/Between.mma | 16 +- .../procedural/Coq/Arith/Bool_nat.mma | 16 +- .../contribs/procedural/Coq/Arith/Compare.mma | 16 +- .../procedural/Coq/Arith/Compare_dec.mma | 16 +- .../contribs/procedural/Coq/Arith/Div.mma | 22 +- .../contribs/procedural/Coq/Arith/Div2.mma | 16 +- .../contribs/procedural/Coq/Arith/EqNat.mma | 16 +- .../contribs/procedural/Coq/Arith/Euclid.mma | 16 +- .../contribs/procedural/Coq/Arith/Even.mma | 16 +- .../procedural/Coq/Arith/Factorial.mma | 16 +- .../contribs/procedural/Coq/Arith/Gt.mma | 16 +- .../contribs/procedural/Coq/Arith/Le.mma | 16 +- .../contribs/procedural/Coq/Arith/Lt.mma | 16 +- .../contribs/procedural/Coq/Arith/Max.mma | 16 +- .../contribs/procedural/Coq/Arith/Min.mma | 16 +- .../contribs/procedural/Coq/Arith/Minus.mma | 16 +- .../contribs/procedural/Coq/Arith/Mult.mma | 16 +- .../procedural/Coq/Arith/Peano_dec.mma | 16 +- .../contribs/procedural/Coq/Arith/Plus.mma | 16 +- .../contribs/procedural/Coq/Arith/Wf_nat.mma | 16 +- .../contribs/procedural/Coq/Bool/Bool.mma | 16 +- .../contribs/procedural/Coq/Bool/BoolEq.mma | 16 +- .../contribs/procedural/Coq/Bool/Bvector.mma | 16 +- .../contribs/procedural/Coq/Bool/DecBool.mma | 16 +- .../contribs/procedural/Coq/Bool/IfProp.mma | 16 +- .../contribs/procedural/Coq/Bool/Sumbool.mma | 16 +- .../contribs/procedural/Coq/Bool/Zerob.mma | 16 +- .../contribs/procedural/Coq/Coq.conf.xml | 2 +- .../matita/contribs/procedural/Coq/Coq.ma | 214 +++--------------- .../procedural/Coq/Init/Datatypes.mma | 16 +- .../contribs/procedural/Coq/Init/Logic.mma | 16 +- .../procedural/Coq/Init/Logic_Type.mma | 16 +- .../procedural/Coq/Init/Notations.mma | 20 +- .../contribs/procedural/Coq/Init/Peano.mma | 16 +- .../contribs/procedural/Coq/Init/Prelude.mma | 16 +- .../contribs/procedural/Coq/Init/Specif.mma | 16 +- .../contribs/procedural/Coq/Init/Wf.mma | 16 +- .../procedural/Coq/IntMap/Adalloc.mma | 16 +- .../contribs/procedural/Coq/IntMap/Addec.mma | 16 +- .../contribs/procedural/Coq/IntMap/Addr.mma | 16 +- .../contribs/procedural/Coq/IntMap/Adist.mma | 16 +- .../procedural/Coq/IntMap/Allmaps.mma | 16 +- .../contribs/procedural/Coq/IntMap/Fset.mma | 16 +- .../contribs/procedural/Coq/IntMap/Lsort.mma | 16 +- .../contribs/procedural/Coq/IntMap/Map.mma | 16 +- .../procedural/Coq/IntMap/Mapaxioms.mma | 16 +- .../contribs/procedural/Coq/IntMap/Mapc.mma | 16 +- .../procedural/Coq/IntMap/Mapcanon.mma | 16 +- .../procedural/Coq/IntMap/Mapcard.mma | 16 +- .../procedural/Coq/IntMap/Mapfold.mma | 16 +- .../procedural/Coq/IntMap/Mapiter.mma | 16 +- .../procedural/Coq/IntMap/Maplists.mma | 16 +- .../procedural/Coq/IntMap/Mapsubset.mma | 16 +- .../contribs/procedural/Coq/Lists/List.mma | 16 +- .../contribs/procedural/Coq/Lists/ListSet.mma | 16 +- .../procedural/Coq/Lists/MonoList.mma | 16 +- .../contribs/procedural/Coq/Lists/Streams.mma | 189 ++++++++++++++++ .../procedural/Coq/Lists/TheoryList.mma | 16 +- .../contribs/procedural/Coq/Logic/Berardi.mma | 18 +- .../procedural/Coq/Logic/ChoiceFacts.mma | 22 +- .../procedural/Coq/Logic/Classical.mma | 16 +- .../procedural/Coq/Logic/ClassicalChoice.mma | 16 +- .../Coq/Logic/ClassicalDescription.mma | 16 +- .../procedural/Coq/Logic/ClassicalFacts.mma | 18 +- .../Coq/Logic/Classical_Pred_Set.mma | 16 +- .../Coq/Logic/Classical_Pred_Type.mma | 16 +- .../procedural/Coq/Logic/Classical_Prop.mma | 16 +- .../procedural/Coq/Logic/Classical_Type.mma | 16 +- .../procedural/Coq/Logic/Decidable.mma | 16 +- .../procedural/Coq/Logic/Diaconescu.mma | 32 +-- .../contribs/procedural/Coq/Logic/Eqdep.mma | 16 +- .../procedural/Coq/Logic/Eqdep_dec.mma | 26 ++- .../contribs/procedural/Coq/Logic/Hurkens.mma | 26 +-- .../contribs/procedural/Coq/Logic/JMeq.mma | 25 +- .../procedural/Coq/Logic/ProofIrrelevance.mma | 22 +- .../procedural/Coq/Logic/RelationalChoice.mma | 18 +- .../contribs/procedural/Coq/NArith/BinNat.mma | 16 +- .../contribs/procedural/Coq/NArith/BinPos.mma | 16 +- .../contribs/procedural/Coq/NArith/NArith.mma | 16 +- .../contribs/procedural/Coq/NArith/Pnat.mma | 16 +- .../contribs/procedural/Coq/Num/AddProps.mma | 50 +--- .../contribs/procedural/Coq/Num/Axioms.mma | 50 ++-- .../procedural/Coq/Num/Definitions.mma | 44 ++-- .../procedural/Coq/Num/DiscrAxioms.mma | 22 +- .../procedural/Coq/Num/DiscrProps.mma | 22 +- .../contribs/procedural/Coq/Num/EqAxioms.mma | 38 +--- .../contribs/procedural/Coq/Num/EqParams.mma | 35 +-- .../contribs/procedural/Coq/Num/GeAxioms.mma | 28 +-- .../contribs/procedural/Coq/Num/GeProps.mma | 14 -- .../contribs/procedural/Coq/Num/GtAxioms.mma | 28 +-- .../contribs/procedural/Coq/Num/GtProps.mma | 14 -- .../contribs/procedural/Coq/Num/LeAxioms.mma | 28 +-- .../contribs/procedural/Coq/Num/LeProps.mma | 82 ++----- .../procedural/Coq/Num/Leibniz/EqAxioms.mma | 47 +--- .../procedural/Coq/Num/Leibniz/NSyntax.mma | 45 ---- .../procedural/Coq/Num/Leibniz/Params.mma | 26 ++- .../contribs/procedural/Coq/Num/LtProps.mma | 70 +----- .../contribs/procedural/Coq/Num/NSyntax.mma | 55 ----- .../procedural/Coq/Num/Nat/Axioms.mma | 49 ++-- .../procedural/Coq/Num/Nat/NSyntax.mma | 41 ---- .../procedural/Coq/Num/Nat/NeqDef.mma | 4 +- .../contribs/procedural/Coq/Num/NeqAxioms.mma | 33 +-- .../contribs/procedural/Coq/Num/NeqDef.mma | 38 +--- .../contribs/procedural/Coq/Num/NeqParams.mma | 25 +- .../contribs/procedural/Coq/Num/NeqProps.mma | 36 +-- .../contribs/procedural/Coq/Num/OppAxioms.mma | 14 -- .../contribs/procedural/Coq/Num/OppProps.mma | 14 -- .../contribs/procedural/Coq/Num/Params.mma | 41 ++-- .../contribs/procedural/Coq/Num/SubProps.mma | 14 -- .../procedural/Coq/Reals/Alembert.mma | 16 +- .../procedural/Coq/Reals/AltSeries.mma | 16 +- .../procedural/Coq/Reals/ArithProp.mma | 16 +- .../procedural/Coq/Reals/Binomial.mma | 16 +- .../procedural/Coq/Reals/Cauchy_prod.mma | 16 +- .../procedural/Coq/Reals/Cos_plus.mma | 16 +- .../contribs/procedural/Coq/Reals/Cos_rel.mma | 16 +- .../contribs/procedural/Coq/Reals/DiscrR.mma | 16 +- .../procedural/Coq/Reals/Exp_prop.mma | 16 +- .../procedural/Coq/Reals/Integration.mma | 16 +- .../contribs/procedural/Coq/Reals/MVT.mma | 16 +- .../procedural/Coq/Reals/NewtonInt.mma | 16 +- .../procedural/Coq/Reals/PSeries_reg.mma | 16 +- .../contribs/procedural/Coq/Reals/PartSum.mma | 16 +- .../contribs/procedural/Coq/Reals/RIneq.mma | 16 +- .../contribs/procedural/Coq/Reals/RList.mma | 16 +- .../contribs/procedural/Coq/Reals/R_Ifp.mma | 16 +- .../contribs/procedural/Coq/Reals/R_sqr.mma | 16 +- .../contribs/procedural/Coq/Reals/R_sqrt.mma | 16 +- .../procedural/Coq/Reals/Ranalysis.mma | 16 +- .../procedural/Coq/Reals/Ranalysis1.mma | 16 +- .../procedural/Coq/Reals/Ranalysis2.mma | 16 +- .../procedural/Coq/Reals/Ranalysis3.mma | 16 +- .../procedural/Coq/Reals/Ranalysis4.mma | 16 +- .../contribs/procedural/Coq/Reals/Raxioms.mma | 16 +- .../contribs/procedural/Coq/Reals/Rbase.mma | 16 +- .../procedural/Coq/Reals/Rbasic_fun.mma | 16 +- .../procedural/Coq/Reals/Rcomplete.mma | 16 +- .../procedural/Coq/Reals/Rdefinitions.mma | 16 +- .../contribs/procedural/Coq/Reals/Rderiv.mma | 16 +- .../contribs/procedural/Coq/Reals/Reals.mma | 16 +- .../procedural/Coq/Reals/Rfunctions.mma | 16 +- .../contribs/procedural/Coq/Reals/Rgeom.mma | 16 +- .../procedural/Coq/Reals/RiemannInt.mma | 16 +- .../procedural/Coq/Reals/RiemannInt_SF.mma | 16 +- .../contribs/procedural/Coq/Reals/Rlimit.mma | 16 +- .../contribs/procedural/Coq/Reals/Rpower.mma | 16 +- .../contribs/procedural/Coq/Reals/Rprod.mma | 16 +- .../contribs/procedural/Coq/Reals/Rseries.mma | 16 +- .../contribs/procedural/Coq/Reals/Rsigma.mma | 16 +- .../procedural/Coq/Reals/Rsqrt_def.mma | 16 +- .../procedural/Coq/Reals/Rtopology.mma | 16 +- .../contribs/procedural/Coq/Reals/Rtrigo.mma | 16 +- .../procedural/Coq/Reals/Rtrigo_alt.mma | 16 +- .../procedural/Coq/Reals/Rtrigo_calc.mma | 16 +- .../procedural/Coq/Reals/Rtrigo_def.mma | 16 +- .../procedural/Coq/Reals/Rtrigo_fun.mma | 16 +- .../procedural/Coq/Reals/Rtrigo_reg.mma | 16 +- .../contribs/procedural/Coq/Reals/SeqProp.mma | 16 +- .../procedural/Coq/Reals/SeqSeries.mma | 16 +- .../procedural/Coq/Reals/SplitAbsolu.mma | 16 +- .../procedural/Coq/Reals/SplitRmult.mma | 16 +- .../procedural/Coq/Reals/Sqrt_reg.mma | 16 +- .../procedural/Coq/Relations/Newman.mma | 24 +- .../Coq/Relations/Operators_Properties.mma | 18 +- .../Coq/Relations/Relation_Definitions.mma | 16 +- .../Coq/Relations/Relation_Operators.mma | 20 +- .../procedural/Coq/Relations/Relations.mma | 16 +- .../procedural/Coq/Relations/Rstar.mma | 16 +- .../procedural/Coq/Setoids/Setoid.mma | 24 +- .../procedural/Coq/Sets/Classical_sets.mma | 16 +- .../procedural/Coq/Sets/Constructive_sets.mma | 16 +- .../contribs/procedural/Coq/Sets/Cpo.mma | 20 +- .../procedural/Coq/Sets/Ensembles.mma | 16 +- .../procedural/Coq/Sets/Finite_sets.mma | 16 +- .../procedural/Coq/Sets/Finite_sets_facts.mma | 16 +- .../contribs/procedural/Coq/Sets/Image.mma | 16 +- .../procedural/Coq/Sets/Infinite_sets.mma | 16 +- .../contribs/procedural/Coq/Sets/Integers.mma | 16 +- .../contribs/procedural/Coq/Sets/Multiset.mma | 16 +- .../procedural/Coq/Sets/Partial_Order.mma | 16 +- .../contribs/procedural/Coq/Sets/Permut.mma | 16 +- .../contribs/procedural/Coq/Sets/Powerset.mma | 16 +- .../Coq/Sets/Powerset_Classical_facts.mma | 16 +- .../procedural/Coq/Sets/Powerset_facts.mma | 16 +- .../procedural/Coq/Sets/Relations_1.mma | 16 +- .../procedural/Coq/Sets/Relations_1_facts.mma | 16 +- .../procedural/Coq/Sets/Relations_2.mma | 16 +- .../procedural/Coq/Sets/Relations_2_facts.mma | 16 +- .../procedural/Coq/Sets/Relations_3.mma | 16 +- .../procedural/Coq/Sets/Relations_3_facts.mma | 16 +- .../contribs/procedural/Coq/Sets/Uniset.mma | 16 +- .../contribs/procedural/Coq/Sorting/Heap.mma | 22 +- .../procedural/Coq/Sorting/Permutation.mma | 22 +- .../procedural/Coq/Sorting/Sorting.mma | 22 +- .../Coq/Wellfounded/Disjoint_Union.mma | 16 +- .../procedural/Coq/Wellfounded/Inclusion.mma | 16 +- .../Coq/Wellfounded/Inverse_Image.mma | 20 +- .../Lexicographic_Exponentiation.mma | 16 +- .../Coq/Wellfounded/Lexicographic_Product.mma | 16 +- .../Coq/Wellfounded/Transitive_Closure.mma | 16 +- .../procedural/Coq/Wellfounded/Union.mma | 16 +- .../Coq/Wellfounded/Well_Ordering.mma | 16 +- .../Coq/Wellfounded/Wellfounded.mma | 16 +- .../contribs/procedural/Coq/ZArith/BinInt.mma | 16 +- .../contribs/procedural/Coq/ZArith/Wf_Z.mma | 20 +- .../contribs/procedural/Coq/ZArith/ZArith.mma | 18 +- .../procedural/Coq/ZArith/ZArith_base.mma | 16 +- .../procedural/Coq/ZArith/ZArith_dec.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zabs.mma | 16 +- .../procedural/Coq/ZArith/Zbinary.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zbool.mma | 16 +- .../procedural/Coq/ZArith/Zcompare.mma | 14 +- .../procedural/Coq/ZArith/Zcomplements.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zdiv.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zeven.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zhints.mma | 16 +- .../procedural/Coq/ZArith/Zlogarithm.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zmin.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zmisc.mma | 16 +- .../contribs/procedural/Coq/ZArith/Znat.mma | 16 +- .../procedural/Coq/ZArith/Znumtheory.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zorder.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zpower.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zsqrt.mma | 16 +- .../contribs/procedural/Coq/ZArith/Zwf.mma | 20 +- .../procedural/Coq/ZArith/auxiliary.mma | 16 +- .../contribs/procedural/Makefile.common | 2 +- 235 files changed, 2101 insertions(+), 2644 deletions(-) create mode 100644 helm/software/matita/contribs/procedural/Coq/Lists/Streams.mma diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index 01bfffa30..5e2c3e23c 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -6,7 +6,9 @@ v8Lexer.cmo: v8Parser.cmi options.cmx v8Lexer.cmx: v8Parser.cmx options.cmx grafite.cmo: types.cmx options.cmx grafite.cmi grafite.cmx: types.cmx options.cmx grafite.cmi -engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx grafite.cmi engine.cmi -engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi +engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx options.cmx grafite.cmi \ + engine.cmi +engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx options.cmx grafite.cmx \ + engine.cmi top.cmo: options.cmx engine.cmi top.cmx: options.cmx engine.cmx diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 8009483f1..120d31fdd 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -23,10 +23,13 @@ * http://cs.unibo.it/helm/. *) -module R = Helm_registry -module X = HExtlib -module T = Types -module G = Grafite +module R = Helm_registry +module X = HExtlib +module T = Types +module G = Grafite +module HP = Http_getter + +module O = Options type script = { name : string; @@ -88,9 +91,12 @@ let set_requires st = let init () = let transcript_dir = Filename.dirname Sys.argv.(0) in let default_registry = Filename.concat transcript_dir "transcript" in - load_registry default_registry + let matita_registry = Filename.concat !O.cwd "matita" in + load_registry default_registry; + load_registry matita_registry; + HP.init () -let make cwd registry = +let make registry = let id x = x in let get_coercions = R.get_list (R.pair id id) in let get_output_type key = @@ -117,8 +123,8 @@ let make cwd registry = scripts = Array.make default_scripts default_script } in let st = {st with - heading_path = Filename.concat cwd st.heading_path; - output_path = Filename.concat cwd st.output_path; + heading_path = Filename.concat !O.cwd st.heading_path; + output_path = Filename.concat !O.cwd st.output_path; } in prerr_endline "reading file names ..."; let st = set_files st in diff --git a/helm/software/components/binaries/transcript/engine.mli b/helm/software/components/binaries/transcript/engine.mli index 5de8db2e6..8016d71cf 100644 --- a/helm/software/components/binaries/transcript/engine.mli +++ b/helm/software/components/binaries/transcript/engine.mli @@ -27,6 +27,6 @@ type status val init: unit -> unit -val make: string -> string -> status +val make: string -> status val produce: status -> unit diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index f5c4a49f8..8776185b8 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -29,8 +29,9 @@ module O = Options module UM = UriManager module NP = CicNotationPp module GP = GrafiteAstPp -module G = GrafiteAst -module H = HExtlib +module G = GrafiteAst +module H = HExtlib +module HG = Http_getter let floc = H.dummy_floc @@ -47,6 +48,7 @@ let out_unexported och head s = let out_line_comment och s = let l = 70 - String.length s in + let l = if l < 0 then 0 else l in let s = Printf.sprintf " %s %s" s (String.make l '*') in out_comment och s @@ -79,7 +81,7 @@ let require value = let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) -let inline (kind, uri, prefix, flavour) = +let inline kind uri prefix flavour = let kind = match kind with | T.Declarative -> G.Declarative | T.Procedural -> G.Procedural None @@ -89,9 +91,14 @@ let inline (kind, uri, prefix, flavour) = let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri +let check och src = + if HG.exists ~local:false src then () else + let msg = "UNAVAILABLE OBJECT: " ^ src in + out_line_comment och msg; + prerr_endline msg + let commit kind och items = let trd (_, _, x) = x in - let trd_rth kind (_, _, x, y, z) = kind, x, y, z in let commit = function | T.Heading heading -> out_preamble och heading | T.Line line -> @@ -103,11 +110,13 @@ let commit kind och items = if !O.comments then out_unexported och "NOTATION" (snd specs) (**) | T.Inline (_, T.Var, src, _, _) -> if !O.comments then out_unexported och "UNEXPORTED" src -(* FG: we do not export variables because we cook the other object +(* FG: we do not export variables because we cook the other objects * let name = UriManager.name_of_uri (UriManager.uri_of_string src) in * out_alias och name src *) - | T.Inline specs -> out_command och (inline (trd_rth kind specs)) + | T.Inline (_, _, src, pre, fl) -> + if !O.getter then check och src; + out_command och (inline kind src pre fl) | T.Section specs -> if !O.comments then out_unexported och "UNEXPORTED" (trd specs) | T.Comment comment -> diff --git a/helm/software/components/binaries/transcript/options.ml b/helm/software/components/binaries/transcript/options.ml index e259494b0..fa36624b2 100644 --- a/helm/software/components/binaries/transcript/options.ml +++ b/helm/software/components/binaries/transcript/options.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +let cwd = ref Filename.current_dir_name + let verbose_parser = ref false let verbose_lexer = ref false @@ -30,3 +32,5 @@ let verbose_lexer = ref false let verbose_escape = ref false let comments = ref true + +let getter = ref false diff --git a/helm/software/components/binaries/transcript/top.ml b/helm/software/components/binaries/transcript/top.ml index 5b3b23473..c92b71512 100644 --- a/helm/software/components/binaries/transcript/top.ml +++ b/helm/software/components/binaries/transcript/top.ml @@ -24,18 +24,20 @@ *) let main = - let cwd = ref Filename.current_dir_name in - let help = "Usage: transcript [ -C ] [ | ]*" in + let help = "Usage: transcript [ -glmpx | -C ] [ | ]*" in let help_C = " set working directory to " in - let help_vp = " verbose parsing" in - let help_vl = " verbose lexing" in - let help_vx = " verbose character escaping" in - let set_cwd dir = cwd := dir in - let process_package package = Engine.produce (Engine.make !cwd package) in - Engine.init (); + let help_g = " check for non existing objects" in + let help_l = " verbose lexing" in + let help_m = " minimal output generation" in + let help_p = " verbose parsing" in + let help_x = " verbose character escaping" in + let set_cwd dir = Options.cwd := dir; Engine.init () in + let process_package package = Engine.produce (Engine.make package) in Arg.parse [ ("-C", Arg.String set_cwd, help_C); - ("-vp", Arg.Set Options.verbose_parser, help_vp); - ("-vl", Arg.Set Options.verbose_lexer, help_vl); - ("-vx", Arg.Set Options.verbose_escape, help_vx); + ("-g", Arg.Set Options.getter, help_g); + ("-l", Arg.Set Options.verbose_lexer, help_l); + ("-m", Arg.Clear Options.comments, help_m); + ("-p", Arg.Set Options.verbose_parser, help_p); + ("-x", Arg.Set Options.verbose_escape, help_x); ] process_package help diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly index 4627cf9a2..721cdd141 100644 --- a/helm/software/components/binaries/transcript/v8Parser.mly +++ b/helm/software/components/binaries/transcript/v8Parser.mly @@ -59,6 +59,7 @@ | "Theorem" -> Some `Theorem | "Definition" -> Some `Definition | "Fixpoint" -> Some `Definition + | "CoFixpoint" -> Some `Definition | "Let" -> Some `Definition | "Scheme" -> Some `Theorem | _ -> assert false diff --git a/helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma b/helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma index 8c9c8f27a..191be9f6c 100644 --- a/helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma +++ b/helm/software/matita/contribs/procedural/Coq/Arith/Arith.mma @@ -16,21 +16,21 @@ include "Coq.ma". -(*#**********************************************************************) +(*#***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Coq cic:/Coq cic:/matita/procedural/Coq - /projects/helm/exportation/V8.0_mowgli_bugfix_branch/theories + /home/fguidi/coq_ufficial_theories/8.0pl2 contribs/procedural/Coq .v procedural diff --git a/helm/software/matita/contribs/procedural/Coq/Coq.ma b/helm/software/matita/contribs/procedural/Coq/Coq.ma index 8b1c5bd3a..eadacbd53 100644 --- a/helm/software/matita/contribs/procedural/Coq/Coq.ma +++ b/helm/software/matita/contribs/procedural/Coq/Coq.ma @@ -345,164 +345,40 @@ Infix "::" := cons (at level 60, right associativity) : list_scope. Infix "++" := app (right associativity, at level 60) : list_scope. *) -(* From Num/Leibniz/EqAxioms **********************************************) - -(* NOTATION -Grammar constr constr1 := -eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ]. -*) - -(* NOTATION -Syntax constr - level 1: - equal [ (eqN $t1 $t2) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ]. -*) - -(* From Num/Leibniz/NSyntax ***********************************************) - -(* NOTATION -Infix 6 "<" lt. -*) - -(* NOTATION -Infix 6 "<=" le. -*) - -(* NOTATION -Infix 6 ">" gt. -*) - -(* NOTATION -Infix 6 ">=" ge. -*) - -(* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. -*) - -(* NOTATION -Syntax constr - level 1: - equal [ (eqN $t1 $t2) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ] - ; - - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. -*) - -(* From Num/Nat/NSyntax ***************************************************) - -(* NOTATION -Infix 6 "<" lt. -*) - -(* NOTATION -Infix 6 "<=" le. -*) - -(* NOTATION -Infix 6 ">" gt. -*) - -(* NOTATION -Infix 6 ">=" ge. -*) - -(* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. -*) - -(* NOTATION -Syntax constr - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. -*) - -(* From Num/EqParams ******************************************************) +(* From NArith/BinNat *****************************************************) (* NOTATION -Grammar constr constr1 := -eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eqN $c $c2) ]. +Infix "+" := Nplus : N_scope. *) (* NOTATION -Syntax constr - level 1: - equal [ (eqN $t1 $t2) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ] -. -*) - -(* From Num/NSyntax *******************************************************) - -(* NOTATION -Infix 6 "<" lt V8only 70. +Infix "*" := Nmult : N_scope. *) (* NOTATION -Infix 6 "<=" le V8only 70. +Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. *) -(* NOTATION -Infix 6 ">" gt V8only 70. -*) +(* From NArith/BinPos *****************************************************) (* NOTATION -Infix 6 ">=" ge V8only 70. +Infix "+" := Pplus : positive_scope. *) (* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. +Infix "-" := Pminus : positive_scope. *) (* NOTATION -Syntax constr - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. +Infix "*" := Pmult : positive_scope. *) -(* From Num/NeqDef ********************************************************) - (* NOTATION -Infix 6 "<>" neq V8only 70. +Infix "/" := Pdiv2 : positive_scope. *) -(* From Num/NeqParams *****************************************************) - (* NOTATION -Infix 6 "<>" neq V8only 70. +Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. *) (* From Reals/RIneq *******************************************************) @@ -635,26 +511,6 @@ Add Setoid Prop iff Prop_S. Notation Le_AsB := (le_AsB A B leA leB). *) -(* From Wellfounded/Lexicographic_Product *********************************) - -(* NOTATION -Notation LexProd := (lexprod A B leA leB). -*) - -(* NOTATION -Notation Symprod := (symprod A B leA leB). -*) - -(* NOTATION -Notation SwapProd := (swapprod A R). -*) - -(* From Wellfounded/Union *************************************************) - -(* NOTATION -Notation Union := (union A R1 R2). -*) - (* From Wellfounded/Lexicographic_Exponentiation **************************) (* NOTATION @@ -689,30 +545,30 @@ Notation Cons := (cons (A:=A)). Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100). *) -(* From Wellfounded/Transitive_Closure ************************************) +(* From Wellfounded/Lexicographic_Product *********************************) (* NOTATION -Notation trans_clos := (clos_trans A R). +Notation LexProd := (lexprod A B leA leB). *) -(* From ZArith/Zdiv *******************************************************) - (* NOTATION -Infix "/" := Zdiv : Z_scope. +Notation Symprod := (symprod A B leA leB). *) (* NOTATION -Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. +Notation SwapProd := (swapprod A R). *) -(* From ZArith/Zpower *****************************************************) +(* From Wellfounded/Transitive_Closure ************************************) (* NOTATION -Infix "^" := Zpower : Z_scope. +Notation trans_clos := (clos_trans A R). *) +(* From Wellfounded/Union *************************************************) + (* NOTATION -Infix "^" := Zpower : Z_scope. +Notation Union := (union A R1 R2). *) (* From ZArith/BinInt *****************************************************) @@ -769,45 +625,29 @@ Notation "x < y < z" := (x < y /\ y < z) : Z_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. *) -(* From ZArith/Znumtheory *************************************************) - -(* NOTATION -Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. -*) - -(* From NArith/BinNat *****************************************************) - -(* NOTATION -Infix "+" := Nplus : N_scope. -*) +(* From ZArith/Zdiv *******************************************************) (* NOTATION -Infix "*" := Nmult : N_scope. +Infix "/" := Zdiv : Z_scope. *) (* NOTATION -Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. *) -(* From NArith/BinPos *****************************************************) - -(* NOTATION -Infix "+" := Pplus : positive_scope. -*) +(* From ZArith/Znumtheory *************************************************) (* NOTATION -Infix "-" := Pminus : positive_scope. +Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. *) -(* NOTATION -Infix "*" := Pmult : positive_scope. -*) +(* From ZArith/Zpower *****************************************************) (* NOTATION -Infix "/" := Pdiv2 : positive_scope. +Infix "^" := Zpower : Z_scope. *) (* NOTATION -Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. +Infix "^" := Zpower : Z_scope. *) diff --git a/helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma b/helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma index 8206df4ed..6adaf9a00 100644 --- a/helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma +++ b/helm/software/matita/contribs/procedural/Coq/Init/Datatypes.mma @@ -16,21 +16,21 @@ include "Coq.ma". -(*#**********************************************************************) +(*#***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* v * The Coq Proof Assistant / The Coq Development Team *) -(* y" (at level 95, no associativity). diff --git a/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma b/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma index f23ce2532..447cb3724 100644 --- a/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma +++ b/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma @@ -16,21 +16,21 @@ include "Coq.ma". -(*#**********************************************************************) +(*#***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop := + | Here : forall x:Stream, P x -> Exists x + | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x. +i*) + +inline procedural "cic:/Coq/Lists/Streams/Exists.ind". + +inline procedural "cic:/Coq/Lists/Streams/ForAll.ind". + +(* UNEXPORTED +Section Co_Induction_ForAll +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/Inv.var +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvThenP.var +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Streams/Stream_Properties/Co_Induction_ForAll/InvIsStable.var +*) + +inline procedural "cic:/Coq/Lists/Streams/ForAll_coind.con" as theorem. + +(* UNEXPORTED +End Co_Induction_ForAll +*) + +(* UNEXPORTED +End Stream_Properties +*) + +(* UNEXPORTED +End Streams +*) + +(* UNEXPORTED +Section Map +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Map/A.var +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Map/B.var +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Map/f.var +*) + +inline procedural "cic:/Coq/Lists/Streams/map.con" as definition. + +(* UNEXPORTED +End Map +*) + +(* UNEXPORTED +Section Constant_Stream +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Constant_Stream/A.var +*) + +(* UNEXPORTED +cic:/Coq/Lists/Streams/Constant_Stream/a.var +*) + +inline procedural "cic:/Coq/Lists/Streams/const.con" as definition. + +(* UNEXPORTED +End Constant_Stream +*) + +(* UNEXPORTED +Unset Implicit Arguments. +*) + diff --git a/helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma b/helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma index ac0cf513c..f97fb98cf 100644 --- a/helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma +++ b/helm/software/matita/contribs/procedural/Coq/Lists/TheoryList.mma @@ -16,21 +16,21 @@ include "Coq.ma". -(*#**********************************************************************) +(*#***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ], [<=] and [>=] will be derived from [<] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_trans.con *******************) inline procedural "cic:/Coq/Num/Axioms/lt_trans.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_anti_refl.con ***************) + inline procedural "cic:/Coq/Num/Axioms/lt_anti_refl.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_x_Sx.con ********************) + inline procedural "cic:/Coq/Num/Axioms/lt_x_Sx.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_S_compat.con ****************) + inline procedural "cic:/Coq/Num/Axioms/lt_S_compat.con". -inline procedural "cic:/Coq/Num/Axioms/lt_add_compat_l.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Axioms/lt_add_compat_l.con ************) -(* UNEXPORTED -Hints Resolve add_sym add_assoc_l add_0_x add_Sx_y S_0_1 lt_x_Sx lt_S_compat - lt_trans lt_anti_refl lt_add_compat_l : num. -*) +inline procedural "cic:/Coq/Num/Axioms/lt_add_compat_l.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma b/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma index f067417b7..76f648cf5 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/Definitions.mma @@ -16,51 +16,47 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* [ (eqN $c $c2) ]. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/EqParams/eqN.con **********************) -(* NOTATION -Syntax constr - level 1: - equal [ (eqN $t1 $t2) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ] -. -*) +inline procedural "cic:/Coq/Num/EqParams/eqN.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma index e2568c5d4..c5d03cfe7 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/GeAxioms.mma @@ -16,37 +16,15 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* =] from [<] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/not_lt_ge.con ****************) inline procedural "cic:/Coq/Num/GeAxioms/not_lt_ge.con". -inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/ge_not_lt.con ****************) -(* UNEXPORTED -Hints Resolve not_lt_ge : num. -*) - -(* UNEXPORTED -Hints Immediate ge_not_lt : num. -*) +inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma index 4ac401472..ccc8303b4 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/GeProps.mma @@ -16,17 +16,3 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* ] from [<] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/not_le_gt.con ****************) inline procedural "cic:/Coq/Num/GtAxioms/not_le_gt.con". -inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/GtAxioms/gt_not_le.con ****************) -(* UNEXPORTED -Hints Resolve not_le_gt : num. -*) - -(* UNEXPORTED -Hints Immediate gt_not_le : num. -*) +inline procedural "cic:/Coq/Num/GtAxioms/gt_not_le.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma index 4ac401472..ccc8303b4 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/GtProps.mma @@ -16,17 +16,3 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* " gt. -*) - -(* NOTATION -Infix 6 ">=" ge. -*) - -(*i Infix 7 "+" plus. i*) - -(* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. -*) - -(* NOTATION -Syntax constr - level 1: - equal [ (eqN $t1 $t2) ] -> [ [ $t1:E [0 1] "=" $t2:E ] ] - ; - - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. -*) - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma index c52856b67..b2d613740 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/Leibniz/Params.mma @@ -16,33 +16,39 @@ include "Coq.ma". -(*i $Id $ i*) - -(*s - Axiomatisation of a numerical set - It will be instantiated by Z and R later on - We choose to introduce many operation to allow flexibility in definition - ([S] is primitive in the definition of [nat] while [add] and [one] - are primitive in the definition -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/N.con ******************) inline procedural "cic:/Coq/Num/Leibniz/Params/N.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/zero.con ***************) + inline procedural "cic:/Coq/Num/Leibniz/Params/zero.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/one.con ****************) + inline procedural "cic:/Coq/Num/Leibniz/Params/one.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/add.con ****************) + inline procedural "cic:/Coq/Num/Leibniz/Params/add.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/S.con ******************) + inline procedural "cic:/Coq/Num/Leibniz/Params/S.con". -(*s Relations, equality is defined separately *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/lt.con *****************) inline procedural "cic:/Coq/Num/Leibniz/Params/lt.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/le.con *****************) + inline procedural "cic:/Coq/Num/Leibniz/Params/le.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/gt.con *****************) + inline procedural "cic:/Coq/Num/Leibniz/Params/gt.con". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Leibniz/Params/ge.con *****************) + inline procedural "cic:/Coq/Num/Leibniz/Params/ge.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma index 408550d88..b771e7af6 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/LtProps.mma @@ -16,103 +16,57 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* " gt V8only 70. -*) - -(* NOTATION -Infix 6 ">=" ge V8only 70. -*) - -(*i Infix 7 "+" plus V8only 50. i*) - -(* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. -*) - -(* NOTATION -Syntax constr - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. -*) - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma index 9450785aa..3f40a129c 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/Nat/Axioms.mma @@ -16,80 +16,61 @@ include "Coq.ma". -(*i $Id: i*) - -(*s Axioms for the basic numerical operations *) - include "Num/Params.ma". include "Num/EqAxioms.ma". include "Num/NSyntax.ma". -(*s Lemmas for [add] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_Sx_y.con ***************) inline procedural "cic:/Coq/Num/Nat/Axioms/add_Sx_y.con" as lemma. -(* UNEXPORTED -Hints Resolve add_Sx_y : nat. -*) - -(*s Lemmas for [add] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_0_x.con ****************) inline procedural "cic:/Coq/Num/Nat/Axioms/add_0_x.con" as lemma. -(* UNEXPORTED -Hints Resolve add_0_x : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_sym.con ****************) inline procedural "cic:/Coq/Num/Nat/Axioms/add_sym.con" as lemma. -(* UNEXPORTED -Hints Resolve add_sym : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_eq_compat.con **********) inline procedural "cic:/Coq/Num/Nat/Axioms/add_eq_compat.con" as lemma. -(* UNEXPORTED -Hints Resolve add_eq_compat : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/add_assoc_l.con ************) inline procedural "cic:/Coq/Num/Nat/Axioms/add_assoc_l.con" as lemma. -(*s Lemmas for [one] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/S_0_1.con ******************) inline procedural "cic:/Coq/Num/Nat/Axioms/S_0_1.con" as lemma. -(*s Lemmas for [<], - properties of [>], [<=] and [>=] will be derived from [<] *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_trans.con ***************) inline procedural "cic:/Coq/Num/Nat/Axioms/lt_trans.con" as lemma. -(* UNEXPORTED -Hints Resolve lt_trans : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con ****************) inline procedural "cic:/Coq/Num/Nat/Axioms/lt_x_Sx.con" as lemma. -(* UNEXPORTED -Hints Resolve lt_x_Sx : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_S_compat.con ************) inline procedural "cic:/Coq/Num/Nat/Axioms/lt_S_compat.con" as lemma. -(* UNEXPORTED -Hints Resolve lt_S_compat : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con ***********) inline procedural "cic:/Coq/Num/Nat/Axioms/lt_eq_compat.con" as lemma. +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con ********) + inline procedural "cic:/Coq/Num/Nat/Axioms/lt_add_compat_l.con" as lemma. +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con ************) + inline procedural "cic:/Coq/Num/Nat/Axioms/lt_Sx_Sy_lt.con" as lemma. -(* UNEXPORTED -Hints Immediate lt_Sx_Sy_lt : nat. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con ***********) inline procedural "cic:/Coq/Num/Nat/Axioms/lt_anti_refl.con" as lemma. diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma index c2b487122..ccc8303b4 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NSyntax.mma @@ -16,44 +16,3 @@ include "Coq.ma". -(*s Syntax for arithmetic *) - -(* NOTATION -Infix 6 "<" lt. -*) - -(* NOTATION -Infix 6 "<=" le. -*) - -(* NOTATION -Infix 6 ">" gt. -*) - -(* NOTATION -Infix 6 ">=" ge. -*) - -(*i Infix 7 "+" plus. i*) - -(* NOTATION -Grammar constr lassoc_constr4 := - squash_sum - [ lassoc_constr4($c1) "+" lassoc_constr4($c2) ] -> - case [$c2] of - (SQUASH $T2) -> - case [$c1] of - (SQUASH $T1) -> [ (sumbool $T1 $T2) ] (* {T1}+{T2} *) - | $_ -> [ (sumor $c1 $T2) ] (* c1+{T2} *) - esac - | $_ -> [ (add $c1 $c2) ] (* c1+c2 *) - esac. -*) - -(* NOTATION -Syntax constr - level 4: - sum [ (add $t1 $t2) ] -> [ [ $t1:E [0 1] "+" $t2:L ] ] -. -*) - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma index eff18dbae..5d99d3db5 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/Nat/NeqDef.mma @@ -16,9 +16,9 @@ include "Coq.ma". -(*s Definition of inequality *) - include "Num/Params.ma". +(* UNAVAILABLE OBJECT: cic:/Coq/Num/Nat/NeqDef/neq.con ********************) + inline procedural "cic:/Coq/Num/Nat/NeqDef/neq.con" as definition. diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma index e7b7e12f1..d7ea7c81e 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/NeqAxioms.mma @@ -16,44 +16,19 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* " neq V8only 70. -*) +inline procedural "cic:/Coq/Num/NeqDef/neq.con" as definition. -(* Proofs of axioms *) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/eq_not_neq.con *****************) inline procedural "cic:/Coq/Num/NeqDef/eq_not_neq.con" as lemma. -(* UNEXPORTED -Hints Immediate eq_not_neq : num. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_sym.con ********************) inline procedural "cic:/Coq/Num/NeqDef/neq_sym.con" as lemma. -(* UNEXPORTED -Hints Resolve neq_sym : num. -*) +(* UNAVAILABLE OBJECT: cic:/Coq/Num/NeqDef/neq_not_neq_trans.con **********) inline procedural "cic:/Coq/Num/NeqDef/neq_not_neq_trans.con" as lemma. -(* UNEXPORTED -Hints Resolve neq_not_neq_trans : num. -*) - diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma index 72d888619..adc658df3 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/NeqParams.mma @@ -16,30 +16,9 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* " neq V8only 70. -*) +inline procedural "cic:/Coq/Num/NeqParams/neq.con". diff --git a/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma b/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma index ff4504d7f..c60ba32af 100644 --- a/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma +++ b/helm/software/matita/contribs/procedural/Coq/Num/NeqProps.mma @@ -16,20 +16,6 @@ include "Coq.ma". -(*#**********************************************************************) - -(* v * The Coq Proof Assistant / The Coq Development Team *) - -(* 0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma b/helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma index 52be1ea66..cea33d8a4 100644 --- a/helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma +++ b/helm/software/matita/contribs/procedural/Coq/Reals/Sqrt_reg.mma @@ -16,21 +16,21 @@ include "Coq.ma". -(*#**********************************************************************) +(*#***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* v * The Coq Proof Assistant / The Coq Development Team *) -(*