aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/apply.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
* Ensuring that patterns of the form pat/constr move the hypotheses replacingGravatar Hugo Herbelin2015-09-08
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
* Example for apply and evars.Gravatar Hugo Herbelin2014-09-10
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* An apply test.Gravatar Hugo Herbelin2014-09-02
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
* Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedGravatar herbelin2011-04-28
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* About "apply in":Gravatar herbelin2008-12-09
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Chgts mineurs:Gravatar herbelin2008-04-03
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* Unification suite: petits affinements pour préserver la compatibilitéGravatar herbelin2007-05-24
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* Correction typoGravatar herbelin2006-11-13
* Ajout de dépliage de l'énoncé, si besoin est, dans apply inGravatar herbelin2006-11-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 20:02:26 +0000