| Commit message (Expand) | Author | Age |
|---|
| * | - Fixes for canonical structure resolution (check that the initial term indee... |  Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Removing dead code, thanks to new OCaml warnings and a bit of scripting. |  Pierre-Marie Pédrot | 2014-04-23 |
| * | Simplifying interface of elimination tactics. They used dummy clausenvs, and | Pierre-Marie Pédrot | 2014-04-22 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 |  Pierre Letouzey | 2014-03-05 |
| * | Tachmach.New is now in Proofview.Goal.enter style. |  aspiwack | 2013-11-02 |
| * | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack | 2013-11-02 |
| * | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
| * | Moving side effects into evar_map. There was no reason to keep another |  ppedrot | 2013-10-05 |
| * | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
| * | State Transaction Machine |  gareuselesinge | 2013-08-08 |
| * | Backtrack on unneeded change of interface for pose_metas_as_evars. |  msozeau | 2013-06-04 |
| * | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau | 2013-06-04 |
| * | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau | 2013-04-18 |
| * | Fix for bug #3017: wrong handling of the unresolvability status | msozeau | 2013-04-03 |
| * | Fixed a little inefficiency of "set/destruct" over a pattern. Now |  herbelin | 2012-12-18 |
| * | Monomorphization (proof) | ppedrot | 2012-11-25 |
| * | 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 |
| * | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau | 2012-06-04 |
| * | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau | 2012-03-20 |
| * | Noise for nothing |  pboutill | 2012-03-02 |
| * | Added a flag to control the use of typing when instantiating applied | herbelin | 2011-12-17 |
| * | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin | 2011-10-11 |
| * | Generalizing flag use_evars_pattern_unification into a flag | herbelin | 2011-06-18 |
| * | Added a flag to restrict conversion in tactic unification on the | herbelin | 2011-06-13 |
| * | Added a new flag for freezing evars in tactic unification. Used this | herbelin | 2011-06-12 |
| * | Moved allow_K to a unification flag | herbelin | 2011-06-10 |
| * | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau | 2011-04-18 |
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Added eta-expansion in kernel, type inference and tactic unification, | herbelin | 2010-09-20 |
| * | In the computation of missing arguments for apply, accept that the | herbelin | 2010-09-17 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | 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 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | - Fixed a bug in checking that implicit arguments are all correctly | herbelin | 2009-09-18 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Reactivation of pattern unification of evars in apply unification, in | herbelin | 2009-07-08 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack | 2009-07-07 |
| * | Backtrack on experimental unification with sort variables: it requires | msozeau | 2009-06-02 |
| * | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
| * | Minor unification changes: | msozeau | 2009-05-18 |
| * | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin | 2009-04-24 |
| * | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
| * | Fix looping class resolution bug discovered by B. Aydemir and use the | msozeau | 2008-12-14 |
| * | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin | 2008-10-26 |
| * | More debugging of handling of open constrs with typeclasses: | msozeau | 2008-10-25 |
Matthieu Sozeau
Pierre-Marie Pédrot
Pierre Letouzey
aspiwack
ppedrot
gareuselesinge
msozeau
herbelin
regisgia
pboutill
glondu
letouzey