| Age | Commit message (Expand) | Author |
|---|
| 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-04-29 | Merging Context and Sign. | ppedrot |
| 2013-02-28 | Repairing r16205: errors raised by check_evar_instance were no longer | 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-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 | 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-03-02 | Noise for nothing | pboutill |
| 2011-04-08 | Replaced printing number of ill-typed branch by printing name of constructor | 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-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-06-12 | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 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-02-21 | Utilisation de l'environnement pour l'affichage de certains messages d'erreurs | herbelin |
| 2006-10-05 | Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ... | notin |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-02-08 | Localisation des erreurs de sorte du prétypage | herbelin |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-09-03 | deplacement de clenv vers pretyping | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-07-16 | Suppression de Rawterm.loc, branchement sur Util.loc | herbelin |
| 2004-07-13 | bug #790: better error_not_clean | barras |
| 2003-09-06 | Paramétrisation vis à vis de existential_key | herbelin |
| 2002-09-03 | pretyping/pretyping.ml | herbelin |
| 2001-12-18 | Nettoyage exceptions liées au vieux Case | herbelin |
| 2001-11-06 | Suppression des local_constraints, des ctxtty et du focus. | clrenard |
| 2001-11-05 | GROS COMMIT: | barras |
