aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ltac.tex
Commit message (Expand)AuthorAge
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Ltac doc: only variables are accepted as message_tokenGravatar glondu2009-09-23
* Clarify documentation of ltac repeatGravatar glondu2009-09-17
* Report de la révision #12200 (bug #2125)Gravatar notin2009-06-22
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Added a note about the ambiguity of the syntax "qualid" in "tacarg"Gravatar herbelin2008-01-05
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* Changed many refman/*.tex files. Put \label and \index commands that immediat...Gravatar emakarov2007-04-17
* doc: typo/english: "is left associating" -> "is left-associative".Gravatar lmamane2007-02-22
* Documentation of tactical "t1 || t2": t2 is executed if t1 fails toGravatar lmamane2007-02-22
* Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsGravatar herbelin2007-02-15
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* MAJ crédits, fresh; documentation apply inGravatar herbelin2006-10-26
* Documentation de lazymatch et des extensions de idtac et failGravatar herbelin2006-07-11
* Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...Gravatar herbelin2006-07-07
* Documentation Print Ltac qualid; documentation du debugger de ltac.Gravatar herbelin2006-07-05
* Documentation 'external'Gravatar herbelin2006-07-05
* Correction comportement clause _ du match goalGravatar herbelin2006-05-05
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23