| Age | Commit message (Expand) | Author |
|---|
| 2011-05-17 | Break circular dependency Proof_global -> Vernacexpr -> Proof_global. | aspiwack |
| 2011-05-17 | Fixes bug in [maximal_unfocus] introduced in r14120. | aspiwack |
| 2011-05-16 | Repair the "Fail" command after recent changes in exception handling | letouzey |
| 2011-05-16 | test-suite: no more ..._beq in the output of the search tests | letouzey |
| 2011-05-16 | Fix order in Search tests. | letouzey |
| 2011-05-16 | Fixed my last patch: these files no longer use nat_beq (automatically | vsiles |
| 2011-05-16 | turn the automatic generation of boolean equality | vsiles |
| 2011-05-15 | Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so). | herbelin |
| 2011-05-15 | Failing instead of switching to the coercion mechanism when VMcast | herbelin |
| 2011-05-15 | Turning Sys_error into error by default instead of anomaly. After all, | herbelin |
| 2011-05-13 | A better procedure for checking presence of undefined evars. | aspiwack |
| 2011-05-13 | The modules in proofs now use the Errors module to explain their exceptions t... | aspiwack |
| 2011-05-13 | A new mechanism to handle errors. | aspiwack |
| 2011-05-13 | New option [Set Bullet Behavior] allows to select the behaviour of bullets. | aspiwack |
| 2011-05-11 | Print Module (Type) M now tries to print more details | letouzey |
| 2011-05-09 | Improved lia + experimental nlia | fbesson |
| 2011-05-09 | remove useless dependancy for csdpcert | fbesson |
| 2011-05-06 | Fixes in the test-suite after modularisation of ZArith and co | letouzey |
| 2011-05-06 | Additionnal fix of romega after modularisation of ZArith | letouzey |
| 2011-05-06 | update of the file list in doc/stdlib | letouzey |
| 2011-05-05 | BinNat: N.binary_rect is now a definition instead of an opaque proof | letouzey |
| 2011-05-05 | Peano recursion for positive: integration of Daniel Schepler's code | letouzey |
| 2011-05-05 | Minimal lemmas about Z.gt, N.gt and co | letouzey |
| 2011-05-05 | Modularisation of Znat, a few name changed elsewhere | letouzey |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | letouzey |
| 2011-05-05 | Modularization of Nnat | letouzey |
| 2011-05-05 | Setoid_ring: some cleanups related with BinPos and BinNat | letouzey |
| 2011-05-05 | Wf.iter_nat becomes Peano.nat_iter (with an implicit arg) | letouzey |
| 2011-05-05 | BinNatDef containing all functions of BinNat, misc adaptations in BinPos | letouzey |
| 2011-05-05 | BinPosDef: a module with all code about positive, later Included in BinPos | letouzey |
| 2011-05-05 | Modularization of BinNat + fixes of stdlib | letouzey |
| 2011-05-05 | Modularization of Pnat | letouzey |
| 2011-05-05 | Modularization of BinPos + fixes in Stdlib | letouzey |
| 2011-05-05 | Definitions of positive, N, Z moved in Numbers/BinNums.v | letouzey |
| 2011-05-05 | Zdiv: results about eqm (the equality modulo some N) under a section | letouzey |
| 2011-05-05 | Better comments and organisation in Datatypes.v | letouzey |
| 2011-05-05 | Extraction: allow extraction foo when foo is an alias notation | letouzey |
| 2011-05-05 | Fix merge, Cumul moved to CUMUL | msozeau |
| 2011-05-05 | Merge branch 'subclasses' into coq-trunk | msozeau |
| 2011-05-04 | First phase removing obsolete support for eta up to conversion in | herbelin |
| 2011-05-03 | As many notation for for vectors as for List. | pboutill |
| 2011-04-29 | when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec. | pboutill |
| 2011-04-29 | Fixed a bug causing inconsistent states during proof editting. | aspiwack |
| 2011-04-29 | Some comments. | aspiwack |
| 2011-04-29 | Typo in test InitSyntax.out | herbelin |
| 2011-04-29 | Choose relative directory over configured directory for coqlib. | pboutill |
| 2011-04-28 | Attempt to use more local doc in coqide | pboutill |
| 2011-04-28 | CHANGES update | pboutill |
| 2011-04-28 | coq_makefile big cleanup | pboutill |
