| Age | Commit message (Expand) | Author |
|---|
| 2014-09-12 | While we don't have a clean alternative to Clenvtac, add a primitive | Matthieu Sozeau |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-06-25 | Putting implicit arguments of Clenv.res_pf right. | Pierre-Marie Pédrot |
| 2014-06-24 | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot |
| 2014-06-24 | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot |
| 2014-06-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot |
| 2014-05-06 | - 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-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-22 | Simplifying interface of elimination tactics. They used dummy clausenvs, and | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 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 |
