| 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 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Repairing r16205: errors raised by check_evar_instance were no longer | herbelin | 2013-02-28 |
* | 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 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | remove many excessive open Util & Errors in mli's | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Replaced printing number of ill-typed branch by printing name of constructor | herbelin | 2011-04-08 |
* | 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 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin | 2010-06-12 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | 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 |
* | Utilisation de l'environnement pour l'affichage de certains messages d'erreurs | herbelin | 2007-02-21 |
* | Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ... | notin | 2006-10-05 |
* | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
* | Localisation des erreurs de sorte du prétypage | herbelin | 2006-02-08 |
* | hiding the meta_map in evar_defs | barras | 2004-09-15 |
* | deplacement de clenv vers pretyping | barras | 2004-09-03 |
* | premiere reorganisation de l\'unification | barras | 2004-09-03 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Suppression de Rawterm.loc, branchement sur Util.loc | herbelin | 2004-07-16 |