aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* Numbers: two more Local Obligation TacticGravatar letouzey2010-01-12
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Numbers: BigN and BigZ get instantiations of all properties about div and modGravatar letouzey2010-01-08
* Numbers: axiomatization + generic properties of abs and sgn.Gravatar letouzey2010-01-08
* Init/Logic: commutativity and associativity of /\ and \/Gravatar letouzey2010-01-08
* NZAxioms plus a compare allows to build an OrderedTypeGravatar letouzey2010-01-08
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Numbers: separation of funs, notations, axioms. Notations via module, without...Gravatar letouzey2010-01-07
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...Gravatar letouzey2010-01-07
* MSetInterface: more modularityGravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O...Gravatar letouzey2010-01-07
* misc improvements in some Structures filesGravatar letouzey2010-01-07
* MSetAVL: hints made local since some of them are quite violent (transitivity)Gravatar letouzey2010-01-07
* Patch on subtyping check of opaque constants.Gravatar soubiran2010-01-06
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ...Gravatar letouzey2010-01-06
* Numbers abstract layer: more Module Type, used especially for divisions.Gravatar letouzey2010-01-05
* Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/NumbersGravatar letouzey2010-01-05
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* Division in Numbers: proofs with less auto (less sensitive to hints, in parti...Gravatar letouzey2010-01-05
* Division in Numbers: factorisation of signaturesGravatar letouzey2010-01-05
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* ZOdiv: fully use generic properties from ZDivTrunc.vGravatar letouzey2009-12-17
* Reverse order of arguments in min_case_strong for better uniformity (and comp...Gravatar letouzey2009-12-17
* Division in Numbers : more properties, new filenames based on a paper by R. B...Gravatar letouzey2009-12-17
* Division in Numbers: more properties proved (still W.I.P.)Gravatar letouzey2009-12-16
* A generic euclidean division in Numbers (Still Work-In-Progress)Gravatar letouzey2009-12-15
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* NZDomain: investigation of the shape of NZ domain, more results about ofnat:n...Gravatar letouzey2009-12-10
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
* integrate MSetToFiniteSet into the compilation (and fix it)Gravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Forgot a file in last commit.Gravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Rename proper to proper_prf to avoid clash with CoRN, Gravatar msozeau2009-12-03
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 00:28:32 +0000