aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ltac.v
Commit message (Expand)AuthorAge
* Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Gravatar Hugo Herbelin2015-10-28
* Fixing #4198 (continued): not matching within the inner lambdas/let-insGravatar Hugo Herbelin2015-10-18
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Adapting ltac output test to new interpretation of binders.Gravatar Hugo Herbelin2014-09-15
* test-suite: Local Tactic Notation is now legal since r15731Gravatar letouzey2012-08-23
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Réparation absence d'interprétation des liaisons vers listesGravatar herbelin2007-02-15
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Applatissement des noeuds application vide dans le filtrage Ltac (ex:Gravatar herbelin2006-10-25
* Test Tactic NotationGravatar herbelin2006-09-22
* Ajout test relatif au bug #984Gravatar herbelin2006-03-05
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* test de la bonne position des vars de ltac entre les vars et les relsGravatar herbelin2005-02-02
* AjoutsGravatar herbelin2004-09-25
* Ajout exemple InstGravatar herbelin2004-03-11
* Test backtrackingGravatar herbelin2003-05-22
* Il ne doit plus y avoir de preuves non terminées à la sortie du fichierGravatar herbelin2003-01-19
* *** empty log message ***Gravatar herbelin2002-06-14
* Test de l'interprétation des fermetures de Match Context (2ème)Gravatar herbelin2002-06-13
* Test de l'interprétation des fermetures de Match ContextGravatar herbelin2002-06-13
* *** empty log message ***Gravatar herbelin2001-12-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 07:45:51 +0000