| Age | Commit message (Expand) | Author |
|---|
| 2010-09-30 | Improve handling of metas as evars in unification (patch by Hugo) | letouzey |
| 2010-09-30 | Speed-up refine by avoiding some calls to Evd.fold | letouzey |
| 2010-09-28 | Fix bug #2321, allowing "_" named projections in classes. Not realizing | msozeau |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-09-28 | Remove "init" label from Termops.it_mk* specialized functions | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-11 | Improving a few error messages in Ltac interpretation | herbelin |
| 2010-08-02 | Fix [clenv_missing] to compute a better approximation of missing | msozeau |
| 2010-07-29 | kernel conversion and reduction do not raise assert failure on ill-typed term... | barras |
| 2010-07-29 | fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate... | barras |
| 2010-07-27 | Minor fixes: | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-23 | Some fine-tuning after removal of automatic imports of coercions in r13310 | herbelin |
| 2010-07-22 | Extension of the recursive notations mechanism | herbelin |
| 2010-07-22 | Made coercions active only when modules are imported. | herbelin |
| 2010-07-18 | Reverted 13293 commited mistakenly. Sorry for the noise. | herbelin |
| 2010-07-18 | Tentative de suppression de l'import automatique des hints et coercions. | herbelin |
| 2010-06-30 | Fix (part of) bug #2347, de Bruijn bug in Program's pretyper. | msozeau |
| 2010-06-29 | Made tclABSTRACT normalize evars before saying it does not support | herbelin |
| 2010-06-28 | Fixed a bug introduced in a combination in r12807 and revealed in | herbelin |
| 2010-06-26 | Applying François' patches about Canonical Projections (see #2302 and #2334). | herbelin |
| 2010-06-25 | Restored a "feature" of unification in pre-8.3 (it was used e.g. in a | herbelin |
| 2010-06-22 | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-06-18 | Hack for fixing bug #2172 (see explanations in file rewrite-2172.v). | herbelin |
| 2010-06-13 | Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine" | herbelin |
| 2010-06-12 | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin |
| 2010-06-12 | Improved the inference of the return predicate in dependent pattern-matching. | herbelin |
| 2010-06-12 | Added rudimentary support for using constructors from the explicit | herbelin |
| 2010-06-12 | Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem). | herbelin |
| 2010-06-11 | Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic). | herbelin |
| 2010-06-10 | Fixed two bugs in pattern-matching compilation | herbelin |
| 2010-06-06 | Added support for Ltac-matching terms with variables bound in the pattern | herbelin |
| 2010-05-28 | Documentation of pretype_id (minor commit). | herbelin |
| 2010-05-26 | Fixing Derive Inversion for new proof engine | herbelin |
| 2010-05-20 | Fix bug 2307 | pboutill |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-05-19 | Remove compile-command pragmas for emacs | letouzey |
| 2010-05-18 | Some ocamldoc comments + Fixing name of .coqrc.version file in refman | pboutill |
| 2010-05-18 | Applicative commutative cuts in Fixpoint guard condition | pboutill |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-05-09 | Added a few informations about file lineages (for the most part in kernel) | herbelin |
| 2010-05-07 | Deux commentaires retirés de ocamldoc. | aspiwack |
| 2010-05-03 | ocamldoc related fixes | pboutill |
| 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-26 | Misc small fixes : warning, dep cycles, ocamlbuild... | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
