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