| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Updating headers. |  herbelin | 2012-08-08 |
| * | Added an indirection with respect to Loc in Compat. As many [open Compat] |  ppedrot | 2012-06-22 |
| * | Glob_term now mli-only, operations now in Glob_ops |  letouzey | 2012-05-29 |
| * | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey | 2012-05-29 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Fixes bug #2654 (tactic instantiate failing to update existential variables). |  aspiwack | 2012-01-06 |
| * | Granted legitimate wish #2607 (not exposing crude fixpoint body of | herbelin | 2011-12-18 |
| * | Propagated information from the reduction tactics to the kernel so | herbelin | 2011-08-10 |
| * | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey | 2011-07-04 |
| * | Catch AbstractionOverMeta as a unification failure in precatchable_exception. |  msozeau | 2011-06-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-07 |
| * | Attempt to preserve casts during a refine, especially VMcast | letouzey | 2010-12-10 |
| * | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proof | herbelin | 2010-07-21 |
| * | Automatic introduction of names given before ":" in Lemma's and | herbelin | 2010-06-09 |
| * | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
| * | Consider OccurCheck a catchable exception. | msozeau | 2010-03-08 |
| * | Errors issued by reduction tactics (e.g. pattern) were not caught by "try". | herbelin | 2010-01-04 |
| * | Add support for remaining side-conditions in "apply in as". | herbelin | 2009-10-25 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | - Fixing bug #2139 (kernel-based test of well-formation of elimination | herbelin | 2009-07-15 |
| * | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin | 2009-06-06 |
| * | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
| * | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
| * | pushed evar reduction in kernel |  barras | 2009-02-06 |
| * | Backporting from v8.2 to trunk: | herbelin | 2009-01-18 |
| * | fixing problem with CompCert: reordering resulting from tac change was not cl... | barras | 2008-11-27 |
| * | closed bug 1898: fold x in x; added a reordering primitive tactic | barras | 2008-11-26 |
| * | Fix for bug #1981, correct the mismatch between the meta types used in | msozeau | 2008-10-25 |
| * | Raise informative errors instead of Failures or anomalies in case a meta | msozeau | 2008-10-24 |
| * | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
| * | fixing r11433 again: | barras | 2008-10-07 |
| * | bug #1951: polymorphic indtypes: universe subst was not performed in the type... | barras | 2008-10-06 |
| * | Correction bug assert (introduit dans la révision 11300) qui ne | herbelin | 2008-09-09 |
| * | More debugging of [Equations], now able to discharge even the heavily | msozeau | 2008-09-07 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Changement de catch_error pour qu'il rattrape les erreurs d'arguments | aspiwack | 2008-06-27 |
| * | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin | 2008-04-30 |
| * | Suite commit 10861 | herbelin | 2008-04-28 |
| * | Petites corrections vis à vis des commits 10860, 10859, 10850 | herbelin | 2008-04-28 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | Mise en place d'une extension de apply pour que celui-ci sache | herbelin | 2008-04-04 |
| * | Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145) | herbelin | 2008-03-10 |
| * | Util.option_compare devient Option.Misc.Compare et change un peu de type | aspiwack | 2007-12-07 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
herbelin
ppedrot
letouzey
pboutill
aspiwack
msozeau
glondu
barras