| Age | Commit message (Expand) | Author |
|---|
| 2018-03-30 | Change Implicit Arguments to Arguments in test-suite | Jasper Hugunin |
| 2016-02-13 | Do not give a name to anonymous evars anymore. See bug #4547. | Pierre-Marie Pédrot |
| 2015-09-08 | Ensuring that patterns of the form pat/constr move the hypotheses replacing | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Fixing test apply.v (had wrong option name). | Hugo Herbelin |
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin |
| 2015-02-23 | Fixing occur-check which was too strong in unification.ml. | Hugo Herbelin |
| 2014-09-29 | Restoring non-uniform delta on local and global constants in 2nd order | Hugo Herbelin |
| 2014-09-10 | Example for apply and evars. | Hugo Herbelin |
| 2014-09-03 | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin |
| 2014-09-02 | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin |
| 2014-09-02 | An apply test. | Hugo Herbelin |
| 2014-08-29 | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin |
| 2014-08-25 | "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-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-16 | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-03-23 | Fix the test-suite by removing any Reset in the scripts | letouzey |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2011-12-17 | Added ability to take the type of applied metas into account when | herbelin |
| 2011-04-28 | Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixed | herbelin |
| 2011-03-13 | Fix inductive_template building ill-typed evars, and update test-suite scripts | msozeau |
| 2010-04-11 | Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto"). | herbelin |
| 2010-01-12 | 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 |
| 2009-12-29 | Improving descend_in_conjunctions (using a combinators instead of a tactic) | herbelin |
| 2009-12-13 | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin |
| 2009-10-25 | 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-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 |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-10-26 | Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui | herbelin |
| 2008-10-19 | Retour en arrière pour raison de compatibilité sur la suppression du nf_evar | herbelin |
| 2008-10-18 | - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429) | herbelin |
| 2008-06-18 | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin |
| 2008-04-28 | Petites corrections vis à vis des commits 10860, 10859, 10850 | herbelin |
| 2008-04-27 | Quelques bricoles autour de l'unification: | herbelin |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-03 | Chgts mineurs: | herbelin |
| 2008-04-01 | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin |
| 2007-05-28 | Contrôle de la compatibilité de apply via une information dans les | herbelin |
| 2007-05-24 | Unification suite: petits affinements pour préserver la compatibilité | herbelin |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2006-12-13 | Alignement de la politique de renommage de rename_bound_var (utilisé pour | herbelin |
| 2006-11-13 | Correction typo | herbelin |
| 2006-11-10 | Ajout de dépliage de l'énoncé, si besoin est, dans apply in | herbelin |
