| Age | Commit message (Expand) | Author |
| 2011-04-28 | coqtop -config returns coq returns coq environments at exection time | pboutill |
| 2011-04-21 | Win32: remove the need for Coq.bat and Coqide.bat | letouzey |
| 2011-04-14 | Add directories in COQPATH to search path. | herbelin |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2011-03-05 | Starting being more explicit on the reasons why module subtyping fails. | herbelin |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-02-11 | An generic imperative union-find, used for deps of evars in Class_tactics | letouzey |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2011-01-25 | Fix compilation with camlp5 (Closes: #2487) | glondu |
| 2011-01-06 | Remove Safe_marshal | glondu |
| 2010-12-25 | Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands | glondu |
| 2010-12-06 | Use !Pp_control.std_ft for printing grammars | glondu |
| 2010-12-03 | Remove dead code | glondu |
| 2010-11-18 | adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6 | letouzey |
| 2010-11-16 | Support for camlp5 6.02.0 (Closes: #2432) | glondu |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-19 | Addressing part 2 of bug report 2377 (removing intrusive warning when | herbelin |
| 2010-09-17 | Coqdep_boot : misc improvements | letouzey |
| 2010-08-31 | * By default, load proof terms. | regisgia |
| 2010-08-27 | * lib/Flags: Replace dont_load_proofs by load_proofs since not loading | regisgia |
| 2010-07-29 | Rather quick hack to make basic unicode notations available by | herbelin |
| 2010-07-29 | Fixed a bug introduced (r13316/r13329) in the printing of notations | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Constrintern: unified push_name_env and push_loc_name_env; made | herbelin |
| 2010-07-20 | Fixed a bug in list_forall2eq (wrong exception was caught). | herbelin |
| 2010-07-02 | Remove dependency to Unix from module Profile | glondu |
| 2010-06-30 | Move [delayed] to util and use [force_delayed] everywhere to force | msozeau |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-06-22 | Protection against anomaly when loading a state with bad magic number. | herbelin |
| 2010-06-21 | Extraction: replace unicode characters in ident by ascii encodings (fix #2158... | letouzey |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-06-08 | Made option "Automatic Introduction" active by default before too many | herbelin |
| 2010-06-08 | Fix treatment of {struct x} annotations in presence of generalized | msozeau |
| 2010-06-01 | restore handling of lexer errors | letouzey |
| 2010-05-31 | CoqIDE goes multiprocess | vgross |
| 2010-05-28 | Account for Stephane Glondu's remarks. | fkirchne |
| 2010-05-28 | Use existing functions to reimplement search_exe. | fkirchne |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-05-19 | Nicer representation of tokens, more independant of camlp* | letouzey |
| 2010-05-19 | Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way | letouzey |
| 2010-05-19 | static (and shared) camlp4use instead of per-file declaration | letouzey |
| 2010-05-19 | Discontinue support for ocaml 3.09.* | letouzey |
| 2010-04-29 | Various minor improvements of comments in mli for ocamldoc | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-27 | Added a new exception for already declared Schemes, | vsiles |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-04-19 | Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). | herbelin |