| Age | Commit message (Expand) | Author |
|---|
| 2014-12-11 | Added a CannotSolveConstraint unification error and made experiments | Hugo Herbelin |
| 2014-12-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-03 | Fixing #3634 (wrong env in "cannot instantiate because not in its | Hugo Herbelin |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-10-22 | Moving potentially costly computation from exception raising to message | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-28 | Repairing r16205: errors raised by check_evar_instance were no longer | herbelin |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-02-17 | Displaying environment and unfolding aliases in "cannot_unify" | herbelin |
| 2013-02-17 | A more informative message when the elimination predicate for | herbelin |
| 2013-02-17 | Locating errors from consider_remaining_unif_problems if possible | herbelin |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-10 | Moved code from Pretype_error to Evarutil | ppedrot |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-04 | Improving error message when abtraction over goal (abstract_list_all | herbelin |
| 2012-09-14 | Partial revert of Yann commit in order to use CLib.List when opening | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-16 | A bit of documentation around cases.ml + ML modules uselessly open | herbelin |
| 2011-03-07 | Reverted commit r13893 about propagation of more informative | herbelin |
| 2011-03-07 | Added propagation of evars unification failure reasons for better | herbelin |
| 2011-03-05 | A few more betaiota on environments and types of error messages. Seems to | herbelin |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | 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-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-01-12 | Removing some betaiota-redexes in error messages (an experiment) | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-04 | Backtrack sur la mémoïsation de nf_evar. | aspiwack |
| 2009-02-27 | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack |
| 2008-04-27 | Quelques bricoles autour de l'unification: | herbelin |
| 2008-04-17 | Bug squashing day ! | msozeau |
| 2008-03-10 | Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145) | herbelin |
| 2008-01-18 | Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ... | msozeau |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-08-27 | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin |
