| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2012-05-30 | Restore compatibility with camlp4 (some missing open Tok) | letouzey |
| 2012-05-29 | Fixed an error display bug in CoqIDE. | ppedrot |
| 2012-05-29 | Re-allow Time Back* (cf discussion on coq-club) | letouzey |
| 2012-05-29 | Some documentation of recent changes concerning interfaces | letouzey |
| 2012-05-29 | remove many excessive open Util & Errors in mli's | letouzey |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | Extend become a mli-only file in intf/ | letouzey |
| 2012-05-29 | Avoid Dumpglob dependency on Lexer | letouzey |
| 2012-05-29 | No need to have Refine amongst Hightactics.cm*a | letouzey |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Split Egrammar into Egramml and Egramcoq | letouzey |
| 2012-05-29 | No more Univ in grammar.cma | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | Stuff about notation_constr (ex-aconstr) now in notation_ops.ml | letouzey |
| 2012-05-29 | slim down a bit genarg.ml (pr_intro_pattern forgotten there) | letouzey |
| 2012-05-29 | Glob_term: minor formatting | letouzey |
