| Commit message (Expand) | Author | Age |
* | Add directories in COQPATH to search path. | herbelin | 2011-04-14 |
* | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey | 2011-04-03 |
* | Starting being more explicit on the reasons why module subtyping fails. | herbelin | 2011-03-05 |
* | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
* | An generic imperative union-find, used for deps of evars in Class_tactics | letouzey | 2011-02-11 |
* | A fine-grain control of inlining at functor application via priority levels | letouzey | 2011-01-31 |
* | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
* | Fix compilation with camlp5 (Closes: #2487) | glondu | 2011-01-25 |
* | Remove Safe_marshal | glondu | 2011-01-06 |
* | Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands | glondu | 2010-12-25 |
* | Use !Pp_control.std_ft for printing grammars | glondu | 2010-12-06 |
* | Remove dead code | glondu | 2010-12-03 |
* | adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6 | letouzey | 2010-11-18 |
* | Support for camlp5 6.02.0 (Closes: #2432) | glondu | 2010-11-16 |
* | Added multiple implicit arguments rules per name. | herbelin | 2010-10-03 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Addressing part 2 of bug report 2377 (removing intrusive warning when | herbelin | 2010-09-19 |
* | Coqdep_boot : misc improvements | letouzey | 2010-09-17 |
* | * By default, load proof terms. | regisgia | 2010-08-31 |
* | * lib/Flags: Replace dont_load_proofs by load_proofs since not loading | regisgia | 2010-08-27 |
* | 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-29 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Constrintern: unified push_name_env and push_loc_name_env; made | herbelin | 2010-07-22 |
* | Fixed a bug in list_forall2eq (wrong exception was caught). | herbelin | 2010-07-20 |
* | Remove dependency to Unix from module Profile | glondu | 2010-07-02 |
* | Move [delayed] to util and use [force_delayed] everywhere to force | msozeau | 2010-06-30 |
* | 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-22 |
* | Extraction: replace unicode characters in ident by ascii encodings (fix #2158... | letouzey | 2010-06-21 |
* | Fixing spelling: pr_coma -> pr_comma | herbelin | 2010-06-12 |
* | 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-08 |
* | restore handling of lexer errors | letouzey | 2010-06-01 |
* | CoqIDE goes multiprocess | vgross | 2010-05-31 |
* | Account for Stephane Glondu's remarks. | fkirchne | 2010-05-28 |
* | Use existing functions to reimplement search_exe. | fkirchne | 2010-05-28 |
* | 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-05-19 |
* | 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-29 |
* | Added a new exception for already declared Schemes, | vsiles | 2010-04-27 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). | herbelin | 2010-04-19 |
* | Util: remove list_split_at which is a clone of list_chop | letouzey | 2010-04-16 |
* | Look for csdp in $PATH at runtime, remove -csdpdir configure option | glondu | 2010-04-11 |