| Commit message (Expand) | Author | Age |
* | Restoring non-uniform delta on local and global constants in 2nd order | Hugo Herbelin | 2014-09-29 |
* | Example for apply and evars. | Hugo Herbelin | 2014-09-10 |
* | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin | 2014-09-03 |
* | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin | 2014-09-02 |
* | An apply test. | Hugo Herbelin | 2014-09-02 |
* | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin | 2014-08-29 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin | 2014-08-25 |
* | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | 2014-08-18 |
* | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin | 2014-08-16 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | Fix the test-suite by removing any Reset in the scripts | letouzey | 2012-03-23 |
* | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin | 2012-03-20 |
* | Added ability to take the type of applied metas into account when | herbelin | 2011-12-17 |
* | Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed | herbelin | 2011-04-28 |
* | Fix inductive_template building ill-typed evars, and update test-suite scripts | msozeau | 2011-03-13 |
* | Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto"). | herbelin | 2010-04-11 |
* | New version of 12650 that was broken (supporting again records when | herbelin | 2010-01-12 |
* | revert commit 12650 for the moment, since it breaks MSetAVL | letouzey | 2010-01-12 |
* | Temporary fix to compensate the loss of descent on dependent | herbelin | 2010-01-12 |
* | Improving descend_in_conjunctions (using a combinators instead of a tactic) | herbelin | 2009-12-29 |
* | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin | 2009-12-13 |
* | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin | 2009-10-25 |
* | 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 |
* | Reactivation of pattern unification of evars in apply unification, in | herbelin | 2009-07-08 |
* | About "apply in": | herbelin | 2008-12-09 |
* | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin | 2008-10-26 |
* | Retour en arrière pour raison de compatibilité sur la suppression du nf_evar | herbelin | 2008-10-19 |
* | - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429) | herbelin | 2008-10-18 |
* | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin | 2008-06-18 |
* | Petites corrections vis à vis des commits 10860, 10859, 10850 | herbelin | 2008-04-28 |
* | Quelques bricoles autour de l'unification: | herbelin | 2008-04-27 |
* | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
* | Chgts mineurs: | herbelin | 2008-04-03 |
* | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin | 2008-04-01 |
* | Contrôle de la compatibilité de apply via une information dans les | herbelin | 2007-05-28 |
* | Unification suite: petits affinements pour préserver la compatibilité | herbelin | 2007-05-24 |
* | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
* | Alignement de la politique de renommage de rename_bound_var (utilisé pour | herbelin | 2006-12-13 |
* | Correction typo | herbelin | 2006-11-13 |
* | Ajout de dépliage de l'énoncé, si besoin est, dans apply in | herbelin | 2006-11-10 |
* | Test apply in | herbelin | 2006-10-24 |