aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Report de la révision #12676Gravatar notin2010-01-15
* Fix uncaught exceptionGravatar vgross2010-01-14
* Document Local Declare ML ModuleGravatar glondu2010-01-14
* 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
* Fix bug #2086, error message when we match on an non-inductive type.Gravatar msozeau2010-01-14
* - Show Obligation TacticGravatar msozeau2010-01-14
* Add *.annot to .gitignoreGravatar glondu2010-01-14
* Disable validateGravatar glondu2010-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
* g_decl_mode: 'by' is now a keywordGravatar letouzey2010-01-12
* Removing some betaiota-redexes in error messages (an experiment)Gravatar herbelin2010-01-12
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
* Typo in error messageGravatar herbelin2010-01-12
* MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)Gravatar letouzey2010-01-12
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-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
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
* Isolation of proof-displaying codeGravatar vgross2010-01-11
* 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
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-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
* Allowed handling of partly-applied record constructors. (Fix for bug #2196.)Gravatar gmelquio2010-01-06
* 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
* use TIMECMD instead of TIME in makefile (unix cmd time reads its format in TIME)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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 17:30:07 +0000