aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
| | | | | | | | | | | | - Local Definitions were considered Global Definitions in globalization file (bug #2288) [I made them "var" which makes them indexed like Variables, should we have an extra category just for Let's?] - the syntax of "[[" was not properly enforced in parse-comments mode - improved documentation of a few vernac file of the library - fixed a bug in Makefile.doc leading to build a bigger and bigger Library.pdf file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)Gravatar herbelin2010-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12888 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake: remove useless tactics abstract_pair, nicer commentsGravatar letouzey2010-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12856 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake: Reorganization, interface for NMake_gen, explicit View, tactic ↵Gravatar letouzey2010-03-10
| | | | | | destr_t, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12855 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlGravatar letouzey2010-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes.Gravatar msozeau2010-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed redundant and ill-named technical lemma.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed SeqProp's dependency on Classical.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Rtrigo's dependency on Classical.Gravatar gmelquio2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Rseries' dependency on Classical.Gravatar gmelquio2010-02-17
| | | | | | | This is a tradeoff: the Archimedean property is used instead through the discrete logarithm. Thanks to P-M. Pedrot for demonstrating this proof scheme on coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12787 85f007b7-540e-0410-9357-904b9bb8a0f7
* RelationClasses: adapt eq_Reflexive and co to avoid Universe InconsistenciesGravatar letouzey2010-02-17
| | | | | | | | We explicitely take care of the argument A to be given to eq_refl,sym,trans when proving that Logic.eq is an instance of Equivalence. This should solve the recent Universe Inconsistencies encountered in CoLoR and FingerTree. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
| | | | | | | | Bvector uses only Minus, so let's avoid loading Arith (and hence ArithRing and hence parts of Z, N) Program.Syntax no longer need Lists now that list is in Datatypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
| | | | | | | This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Rlimit's dependency on Classical.Gravatar gmelquio2010-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed Rderiv's dependency on Classical.Gravatar gmelquio2010-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation Sorting/Mergesort and Structures/OrdersGravatar letouzey2010-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12772 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompSpec2Type is used to build functions, it should be Defined, not QedGravatar letouzey2010-02-13
| | | | | | This solves in particular the compilation failure of contrib ATBR git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12765 85f007b7-540e-0410-9357-904b9bb8a0f7
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
| | | | | | | | | | | In interfaces fields like compare_spec, a CompSpec is prefered to get nice extraction, but then no "destruct (compare_spec .. ..)" is possible in a Type context. Now you can say there "destruct (CompSpec2Type (compare_spec ... ...))" This translate to the Type variant, and make the analysis on it (which is equivalent to analysing the comparison directly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup in Classes, removing unsupported code.Gravatar msozeau2010-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Min, Max: for avoiding inelegant NPeano.max printing, we Export this libGravatar letouzey2010-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Euclidean division for NArithGravatar letouzey2010-02-10
| | | | | | | | | There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We higlight it by putting it in a separate file, prove its specification without using Z (but for the moment can't avoid a detour via nat, though), and then instantiate general results from Natural/Abstract/NDiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
| | | | | | | | | With these properties, we can kill Arith/MinMax, NArith/Nminmax, and leave ZArith/Zminmax as a compatibility file only. Now the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN contains all theses facts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
* NSub: a missing lemma (sub usually decreases)Gravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12716 85f007b7-540e-0410-9357-904b9bb8a0f7
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Records of operations and specs in CyclicAxioms are now type classes (under a module ZnZ for qualification). We benefit from inference and from generic names: (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y). - Beware of typeclasses unfolds: the line about Typeclasses Opaque w1 w2 ... is critical for decent compilation time (x2.5 without it). - Functions defined via same_level are now obtained from a generic version by (Eval ... in ...) during definition. The code obtained this way should be just as before, apart from some (minor?) details. Proofs for these functions are _way_ simplier and lighter. - The macro-generated NMake_gen.v contains only generic iterators and compare, mul, div_gt, mod_gt. I hope to be able to adapt these functions as well soon. - Spec of comparison is now fully done with respect to Zcompare - A log2 function has been added. - No more unsafe_shiftr, we detect the underflow directly with sub_c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
| | | | | | | of cleanup in tactics/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.SGravatar letouzey2010-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for generalized rewriting under dependent binders, using theGravatar msozeau2010-01-26
| | | | | | | [forall_relation] combinator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12691 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
| | | | | | | | we export the "safe" version of these functions, working for all input and not only reasonably small shifting arg. The former "unsafe" shiftr and shiftl are now unsafe_shiftr and unsafe_shiftl. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12688 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
| | | | | | | The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake_gen: fix previous commit (some spaces were critical), remove some more ↵Gravatar letouzey2010-01-19
| | | | | | spaces git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12684 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake_gen: no more spaces at end of linesGravatar letouzey2010-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12683 85f007b7-540e-0410-9357-904b9bb8a0f7
* More improvements of BigN, BigZ, BigQ:Gravatar letouzey2010-01-18
| | | | | | | | | | | | | | | - ring/field: detection of constants for ring/field, detection of power, potential use of euclidean division. - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify. By the way, BigN.zify could still be improved (no insertion of positivity hyps yet, unlike the original zify). - debug of BigQ.qify (autorewrite was looping on spec_0). - for BigQ, start of a generic functor of properties QProperties. - BigQ now implements OrderedType, TotalOrder, and contains facts about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
| | | | | | | | | | | | | | | | | | | | | We use the <+ operation to regroup all known facts about BigN (resp BigZ, ...) in a unique module. This uses also the new ! feature for controling inlining. By the way, we also make sure that these new BigN and BigZ modules implements OrderedTypeFull and TotalOrder, and also contains facts about min and max (cf. GenericMinMax). Side effects: - In NSig and ZSig, specification of compare and eq_bool is now done with respect to Zcompare and Zeq_bool, as for other ops. The order <= and < are also defined via Zle and Zlt, instead of using compare. Min and max are axiomatized instead of being macros. - Some proofs rework in QMake - QOrderedType and Qminmax were in fact not compiled by make world Still todo: OrderedType + MinMax for BigQ, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename Zbinary into Zdigit in order to avoid confusion with ↵Gravatar letouzey2010-01-14
| | | | | | Numbers/.../ZBinary.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to avoid re-declaring Equivalence, especially for Logic.eqGravatar letouzey2010-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12662 85f007b7-540e-0410-9357-904b9bb8a0f7
* GenericMinMax: still a min_case_strong with hypothesis in the wrong orderGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12661 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)Gravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12656 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers/.../NDefOps: one more property about ltbGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: some more proofs about sub,add,le,lt for natural numbersGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: two more Local Obligation TacticGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
| | | | | | | | Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 12:30:12 +0000