| Age | Commit message (Expand) | Author |
|---|
| 2010-01-25 | NMake: several things need not be macro-generated | letouzey |
| 2010-01-19 | Ring31 : a ring structure and tactic for int31 | letouzey |
| 2010-01-19 | NMake_gen: fix previous commit (some spaces were critical), remove some more ... | letouzey |
| 2010-01-19 | NMake_gen: no more spaces at end of lines | letouzey |
| 2010-01-19 | Various bug fix on recent features of the module system: | soubiran |
| 2010-01-18 | More improvements of BigN, BigZ, BigQ: | letouzey |
| 2010-01-17 | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey |
| 2010-01-17 | Simplification of OrdersTac thanks to the functor application ! with no inline | letouzey |
| 2010-01-17 | Variant !F M for functor application that does not honor the Inline declarations | letouzey |
| 2010-01-15 | Report de la révision #12676 | notin |
| 2010-01-14 | Fix uncaught exception | vgross |
| 2010-01-14 | Document Local Declare ML Module | glondu |
| 2010-01-14 | Avoid some more re-declarations of Equivalence instances | letouzey |
| 2010-01-14 | Rename Zbinary into Zdigit in order to avoid confusion with Numbers/.../ZBina... | letouzey |
| 2010-01-14 | Fix bug #2086, error message when we match on an non-inductive type. | msozeau |
| 2010-01-14 | - Show Obligation Tactic | msozeau |
| 2010-01-14 | Add *.annot to .gitignore | glondu |
| 2010-01-14 | Disable validate | glondu |
| 2010-01-13 | Try to avoid re-declaring Equivalence, especially for Logic.eq | letouzey |
| 2010-01-12 | GenericMinMax: still a min_case_strong with hypothesis in the wrong order | letouzey |
| 2010-01-12 | g_decl_mode: 'by' is now a keyword | letouzey |
| 2010-01-12 | Removing some betaiota-redexes in error messages (an experiment) | herbelin |
| 2010-01-12 | New version of 12650 that was broken (supporting again records when | herbelin |
| 2010-01-12 | Typo in error message | herbelin |
| 2010-01-12 | MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu) | letouzey |
| 2010-01-12 | Added module sharing support for typeclasses and hints (pri_auto_tactic). | soubiran |
| 2010-01-12 | Numbers/.../NDefOps: one more property about ltb | letouzey |
| 2010-01-12 | Numbers: some more proofs about sub,add,le,lt for natural numbers | letouzey |
| 2010-01-12 | Numbers: two more Local Obligation Tactic | letouzey |
| 2010-01-12 | revert commit 12650 for the moment, since it breaks MSetAVL | letouzey |
| 2010-01-12 | Temporary fix to compensate the loss of descent on dependent | herbelin |
| 2010-01-11 | Revert "Isolation of proof-displaying code" | vgross |
| 2010-01-11 | Isolation of proof-displaying code | vgross |
| 2010-01-11 | Support "Local Obligation Tactic" (now the default in sections). | msozeau |
| 2010-01-08 | Numbers: BigN and BigZ get instantiations of all properties about div and mod | letouzey |
| 2010-01-08 | * Segmenttree: New. A very simple implementation of segment trees. | regisgia |
| 2010-01-08 | Numbers: axiomatization + generic properties of abs and sgn. | letouzey |
| 2010-01-08 | Init/Logic: commutativity and associativity of /\ and \/ | letouzey |
| 2010-01-08 | NZAxioms plus a compare allows to build an OrderedType | letouzey |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Include can accept both Module and Module Type | letouzey |
| 2010-01-07 | Numbers: separation of funs, notations, axioms. Notations via module, without... | letouzey |
| 2010-01-07 | Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni... | letouzey |
| 2010-01-07 | MSetInterface: more modularity | letouzey |
| 2010-01-07 | OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with... | letouzey |
| 2010-01-07 | DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O... | letouzey |
| 2010-01-07 | misc improvements in some Structures files | letouzey |
| 2010-01-07 | MSetAVL: hints made local since some of them are quite violent (transitivity) | letouzey |
| 2010-01-06 | Allowed handling of partly-applied record constructors. (Fix for bug #2196.) | gmelquio |
| 2010-01-06 | Patch on subtyping check of opaque constants. | soubiran |
