| Age | Commit message (Expand) | Author |
|---|
| 2010-02-03 | fix commit 12706 + comments. | soubiran |
| 2010-02-02 | Small fix on module inclusion. | soubiran |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2010-01-29 | Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.S | letouzey |
| 2010-01-29 | minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t | letouzey |
| 2010-01-28 | Remove bashisms | glondu |
| 2010-01-28 | New command Declare Reduction <id> := <conv_expr>. | letouzey |
| 2010-01-28 | Fix previous commit | notin |
| 2010-01-28 | Fix implicit_application for let-bound variables in the class context. | msozeau |
| 2010-01-28 | Typo in previous commit | notin |
| 2010-01-28 | Correction du bug #2219: application du patch envoyé par F. Garillot | notin |
| 2010-01-28 | Backport fixes in Instance declarations to Program Instance. | msozeau |
| 2010-01-26 | Support for generalized rewriting under dependent binders, using the | msozeau |
| 2010-01-26 | Quick fix for references to section variables unbound in the current | msozeau |
| 2010-01-26 | Add [Next Obligation with tactic] support (wish #1953). | msozeau |
| 2010-01-26 | make init + NMake.v/NMake_gen.v | notin |
| 2010-01-26 | Add -makecmd configure option | glondu |
| 2010-01-25 | NMake (and hence BigN): shiftr, shiftl now in the signature NSig | letouzey |
| 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 |
