| Age | Commit message (Expand) | Author |
|---|
| 2013-11-02 | 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-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-06-04 | 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-04-18 | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau |
| 2013-04-03 | Fix for bug #3017: wrong handling of the unresolvability status | msozeau |
| 2012-12-18 | Fixed a little inefficiency of "set/destruct" over a pattern. Now | herbelin |
| 2012-11-25 | Monomorphization (proof) | ppedrot |
| 2012-09-14 | 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-08-08 | Updating headers. | herbelin |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-17 | Added a flag to control the use of typing when instantiating applied | herbelin |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-06-18 | Generalizing flag use_evars_pattern_unification into a flag | herbelin |
| 2011-06-13 | Added a flag to restrict conversion in tactic unification on the | herbelin |
| 2011-06-12 | Added a new flag for freezing evars in tactic unification. Used this | herbelin |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-04-18 | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-17 | In the computation of missing arguments for apply, accept that the | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-08 | Reactivation of pattern unification of evars in apply unification, in | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-02 | Backtrack on experimental unification with sort variables: it requires | msozeau |
| 2009-05-23 | A try at using sort variables during unification. Instead of refreshing | msozeau |
| 2009-05-18 | Minor unification changes: | msozeau |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-02-19 | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack |
| 2008-12-14 | Fix looping class resolution bug discovered by B. Aydemir and use the | msozeau |
| 2008-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-25 | More debugging of handling of open constrs with typeclasses: | msozeau |
| 2008-10-24 | Raise informative errors instead of Failures or anomalies in case a meta | msozeau |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-04-27 | - Backtrack sur option with_types suite à confusion sur l'utilisation | herbelin |
| 2008-04-26 | - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec | herbelin |
