aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-ltac.tex
AgeCommit message (Expand)Author
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-03Silence some warning about references in documentation.Guillaume Melquiond
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-02Documentation for the backtracking features.aspiwack
2013-08-08Manual fixed w.r.t. STMgareuselesinge
2013-05-29Documenting the "appcontext" by default.ppedrot
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
2011-11-29Documentation of appcontextletouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2010-10-05(Hopefully) clearer explanation of Ltac's context patternsglondu
2009-11-03Report de la révision #12208 de la v8.2 (correction du bug #2126)notin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-09-23Ltac doc: only variables are accepted as message_tokenglondu
2009-09-17Clarify documentation of ltac repeatglondu
2009-06-22Report de la révision #12200 (bug #2125)notin
2009-01-27- Fixed various Overfull in documentation.herbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-05Added a note about the ambiguity of the syntax "qualid" in "tacarg"herbelin
2008-01-05Standardisation du format des références croisées vers Figure, Section, Ch...herbelin
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that immediat...emakarov
2007-02-22doc: typo/english: "is left associating" -> "is left-associative".lmamane
2007-02-22Documentation of tactical "t1 || t2": t2 is executed if t1 fails tolmamane
2007-02-15Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lorsherbelin
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2006-10-26MAJ crédits, fresh; documentation apply inherbelin
2006-07-11Documentation de lazymatch et des extensions de idtac et failherbelin
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...herbelin
2006-07-05Documentation Print Ltac qualid; documentation du debugger de ltac.herbelin
2006-07-05Documentation 'external'herbelin
2006-05-05Correction comportement clause _ du match goalherbelin
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 07:24:10 +0000