| Age | Commit message (Expand) | Author |
|---|
| 2012-06-20 | Install compat5 module with grammar.cma | pboutill |
| 2012-06-20 | Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ... | pboutill |
| 2012-06-20 | Bug 2823: update INSTALL.ide in order to ask for lablgtksourceview | pboutill |
| 2012-06-19 | Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri... | msozeau |
| 2012-06-19 | Fix bug #2695: infinite loop in dependent destruction. | msozeau |
| 2012-06-19 | BinInt: a forgotten scope for a notation | letouzey |
| 2012-06-19 | Fixing printing of @f with no arguments | herbelin |
| 2012-06-19 | Fixing some inconsistencies of constr printer wrt constr parser | herbelin |
| 2012-06-18 | Proof using: nested sections bugfix | gareuselesinge |
| 2012-06-15 | Reductionops abstract machine uses Zcase & Zfix stack node. | pboutill |
| 2012-06-15 | Reductionops : Better abstract machine stack utilities | pboutill |
| 2012-06-15 | Fix coqide vernac lexer | pboutill |
| 2012-06-15 | Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN | pboutill |
| 2012-06-14 | Constrextern is allow to use partially applied notations | pboutill |
| 2012-06-14 | Internalization of pattern is done in two phases. | pboutill |
| 2012-06-14 | coq_makefile fixup | pboutill |
| 2012-06-13 | Fixing annoying autocompletion when deleting text. | ppedrot |
| 2012-06-12 | make sure that documentation compilation works after adding files for | bertot |
| 2012-06-12 | New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles | pboutill |
| 2012-06-12 | bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfully | pboutill |
| 2012-06-12 | Fixing test-suite after last storm in Pp. | pboutill |
| 2012-06-12 | Getting rid of Pcoq remains. | ppedrot |
| 2012-06-12 | Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files. | ppedrot |
| 2012-06-11 | These files are displaced from Rtrigo.v and Ranalysis_reg.v | bertot |
| 2012-06-11 | finish the rearrangement for removing the sin_PI2 axiom. This new version | bertot |
| 2012-06-11 | Adds the proof of PI_ineq, plus some other smarter ways to approximate PI | bertot |
| 2012-06-07 | Colorization of coqtop messages is turned *off* by default | letouzey |
| 2012-06-05 | CHANGES: mention the end of induction principles for records | letouzey |
| 2012-06-05 | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot |
| 2012-06-04 | A box to pretty-print them all. | ppedrot |
| 2012-06-04 | Fixing previous commit (something strange happened...) | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-04 | Added a color output to Coqtop. | ppedrot |
| 2012-06-04 | Separated notice vs info messages, and cleaned up the interface a bit. | ppedrot |
| 2012-06-04 | Fixing #2803. | ppedrot |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-06-02 | Fixed printing error problem... A line had disappeared in a previous patch. | ppedrot |
| 2012-06-02 | Flushing formatters before program exit. | ppedrot |
| 2012-06-01 | More cleaning | ppedrot |
| 2012-06-01 | Cleaning Pp.ppnl use | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-06-01 | Let's try to avoid generating induction principles for records (wish #2693) | letouzey |
| 2012-06-01 | list_eq_dec now transparent (wish #2786) | letouzey |
| 2012-06-01 | Cancel the start of a proof if its init_tac fails (fix #2799) | letouzey |
| 2012-05-31 | tactic is_fix, akin to is_evar, is_hyp, is_ ... family | pboutill |
| 2012-05-31 | Coq_makefile bug for plugins | pboutill |
| 2012-05-30 | Functions *_beq aren't generated anymore, remove comments about them | letouzey |
| 2012-05-30 | Adds Reference-Manual.out to .gitignore | letouzey |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-30 | More uniformisation in Pp.warn functions. | ppedrot |
