| Commit message (Expand) | Author | Age |
|---|
| * | apply zeta reduction before syntaxification |  fbesson | 2011-05-18 |
| * | Extraction: avoid printing of Recursive Extraction in coqide's console |  letouzey | 2011-05-18 |
| * | Coqide: allow the use of Abort (grant wish #2357) | letouzey | 2011-05-18 |
| * | Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR) | letouzey | 2011-05-17 |
| * | Modops: the strengthening functions can work without any env argument | letouzey | 2011-05-17 |
| * | More work on error handling | letouzey | 2011-05-17 |
| * | Add simple test of bullet behaviour. |  aspiwack | 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-17 |
| * | 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-16 |
| * | 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-15 |
| * | 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-13 |
| * | Print Module (Type) M now tries to print more details | letouzey | 2011-05-11 |
| * | Improved lia + experimental nlia | fbesson | 2011-05-09 |
| * | remove useless dependancy for csdpcert | fbesson | 2011-05-09 |
| * | 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-06 |
| * | 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-05 |
| * | First phase removing obsolete support for eta up to conversion in | herbelin | 2011-05-04 |
| * | As many notation for for vectors as for List. |  pboutill | 2011-05-03 |
| * | when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec. | pboutill | 2011-04-29 |
fbesson
letouzey
aspiwack
vsiles
herbelin
msozeau
pboutill