aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Granting wish #2229 (InA_dec transparent) and Michael Day's coq-clubGravatar herbelin2010-04-10
* Change definition of FSetList so that equality is LeibnizGravatar glondu2010-04-09
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
* Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)Gravatar herbelin2010-03-28
* NMake: remove useless tactics abstract_pair, nicer commentsGravatar letouzey2010-03-10
* NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...Gravatar letouzey2010-03-10
* NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlGravatar letouzey2010-03-10
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
* Minor fixes.Gravatar msozeau2010-03-05
* Removed redundant and ill-named technical lemma.Gravatar gmelquio2010-02-18
* Removed SeqProp's dependency on Classical.Gravatar gmelquio2010-02-18
* Removed Rtrigo's dependency on Classical.Gravatar gmelquio2010-02-18
* Removed Rseries' dependency on Classical.Gravatar gmelquio2010-02-17
* RelationClasses: adapt eq_Reflexive and co to avoid Universe InconsistenciesGravatar letouzey2010-02-17
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
* Removed Rlimit's dependency on Classical.Gravatar gmelquio2010-02-17
* Removed Rderiv's dependency on Classical.Gravatar gmelquio2010-02-17
* Uniformisation Sorting/Mergesort and Structures/OrdersGravatar letouzey2010-02-16
* CompSpec2Type is used to build functions, it should be Defined, not QedGravatar letouzey2010-02-13
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Cleanup in Classes, removing unsupported code.Gravatar msozeau2010-02-11
* Min, Max: for avoiding inelegant NPeano.max printing, we Export this libGravatar letouzey2010-02-10
* Euclidean division for NArithGravatar letouzey2010-02-10
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* NSub: a missing lemma (sub usually decreases)Gravatar letouzey2010-02-09
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.SGravatar letouzey2010-01-29
* Support for generalized rewriting under dependent binders, using theGravatar msozeau2010-01-26
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* NMake_gen: fix previous commit (some spaces were critical), remove some more ...Gravatar letouzey2010-01-19
* NMake_gen: no more spaces at end of linesGravatar letouzey2010-01-19
* More improvements of BigN, BigZ, BigQ:Gravatar letouzey2010-01-18
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
* Avoid some more re-declarations of Equivalence instancesGravatar letouzey2010-01-14
* Rename Zbinary into Zdigit in order to avoid confusion with Numbers/.../ZBina...Gravatar letouzey2010-01-14
* Try to avoid re-declaring Equivalence, especially for Logic.eqGravatar letouzey2010-01-13
* GenericMinMax: still a min_case_strong with hypothesis in the wrong orderGravatar letouzey2010-01-12
* MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)Gravatar letouzey2010-01-12
* Numbers/.../NDefOps: one more property about ltbGravatar letouzey2010-01-12
* Numbers: some more proofs about sub,add,le,lt for natural numbersGravatar letouzey2010-01-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 02:45:18 +0000