| Commit message (Expand) | Author | Age |
* | 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-30 |
* | 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-28 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Added eta-expansion in kernel, type inference and tactic unification, | herbelin | 2010-09-20 |
* | Improving a few error messages in Ltac interpretation | herbelin | 2010-09-11 |
* | Fix [clenv_missing] to compute a better approximation of missing | msozeau | 2010-08-02 |
* | 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-29 |
* | Minor fixes: | msozeau | 2010-07-27 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Some fine-tuning after removal of automatic imports of coercions in r13310 | herbelin | 2010-07-23 |
* | Extension of the recursive notations mechanism | herbelin | 2010-07-22 |
* | Made coercions active only when modules are imported. | herbelin | 2010-07-22 |
* | 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-07-18 |
* | Fix (part of) bug #2347, de Bruijn bug in Program's pretyper. | msozeau | 2010-06-30 |
* | Made tclABSTRACT normalize evars before saying it does not support | herbelin | 2010-06-29 |
* | Fixed a bug introduced in a combination in r12807 and revealed in | herbelin | 2010-06-28 |
* | Applying François' patches about Canonical Projections (see #2302 and #2334). | herbelin | 2010-06-26 |
* | Restored a "feature" of unification in pre-8.3 (it was used e.g. in a | herbelin | 2010-06-25 |
* | 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-22 |
* | Hack for fixing bug #2172 (see explanations in file rewrite-2172.v). | herbelin | 2010-06-18 |
* | Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine" | herbelin | 2010-06-13 |
* | 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-12 |
* | Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic). | herbelin | 2010-06-11 |
* | Fixed two bugs in pattern-matching compilation | herbelin | 2010-06-10 |
* | Added support for Ltac-matching terms with variables bound in the pattern | herbelin | 2010-06-06 |
* | Documentation of pretype_id (minor commit). | herbelin | 2010-05-28 |
* | Fixing Derive Inversion for new proof engine | herbelin | 2010-05-26 |
* | Fix bug 2307 | pboutill | 2010-05-20 |
* | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
* | Remove compile-command pragmas for emacs | letouzey | 2010-05-19 |
* | 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-18 |
* | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
* | Added a few informations about file lineages (for the most part in kernel) | herbelin | 2010-05-09 |
* | Deux commentaires retirés de ocamldoc. | aspiwack | 2010-05-07 |
* | ocamldoc related fixes | pboutill | 2010-05-03 |
* | 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 |
* | Misc small fixes : warning, dep cycles, ocamlbuild... | letouzey | 2010-04-26 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |