aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RefMan-tac.tex
Commit message (Expand)AuthorAge
* clausesGravatar barras2004-04-06
* clausesGravatar barras2004-04-06
* MAJ passage coqart a la nouvelle syntaxe de autorewrite et hint rewriteGravatar herbelin2004-03-24
* Hint Rewrite, ancienne syntaxeGravatar herbelin2004-03-19
* MAJ autorewrite/Hint RewriteGravatar herbelin2004-03-17
* Ajout stepl et steprGravatar herbelin2004-03-10
* Ajout 'replace in'Gravatar herbelin2004-03-01
* Modification of the documentation of functional induction/Scheme.Gravatar coq2004-02-06
* ajout d'une passe de latex our avoir un index correctGravatar barras2004-01-14
* Erreurs de derniere minuteGravatar corbinea2004-01-06
* Nouvelle relectureGravatar herbelin2004-01-05
* correction bugs commit precedent et mise en forme htmlGravatar coq2004-01-05
* modif generales claudeGravatar coq2003-12-30
* *** empty log message ***Gravatar barras2003-12-24
* Ajout intro-pattern des inductifs unaireGravatar herbelin2003-12-23
* *** empty log message ***Gravatar barras2003-12-23
* Ajout symmetry in; NArithRing; Hint Local; MAJ V8; typosGravatar herbelin2003-12-21
* TypoGravatar herbelin2003-12-20
* Correction de la grammaire des intro-patternsGravatar herbelin2003-12-19
* Documentation 'inversion as'Gravatar herbelin2003-12-19
* *** empty log message ***Gravatar barras2003-12-19
* *** empty log message ***Gravatar barras2003-12-19
* Petits changements dans la doc de functional scheme et functional induction.Gravatar coq2003-12-19
* COQBIN plus necessaire, typosGravatar marche2003-12-19
* passe sur les labels et les refs dans chapitres tactiquesGravatar filliatr2003-12-19
* premiere passe V8Gravatar filliatr2003-12-18
* encore un peu de tactiques...Gravatar filliatr2003-12-18
* encore un peu de tactiques...Gravatar filliatr2003-12-17
* MAJ induction/destruct/simplGravatar herbelin2003-12-17
* tactiquesGravatar filliatr2003-12-16
* typoGravatar marche2003-12-12
* relecture JCFGravatar filliatr2003-12-02
* added Firstordre and CongruenceGravatar corbinea2003-12-02
* Label redondantGravatar herbelin2003-11-23
* Added a tactic entry for Jprover + commented out inputenc in the main fileGravatar corbinea2003-10-30
* MAJ Double Inductive vis a vis de la V7.4Gravatar herbelin2003-10-27
* passage V8Gravatar filliatr2003-09-25
* Added the documentation on Functional Scheme (a command, I also putGravatar courtieu2003-06-21
* Ajout 'in (Type of ...)'Gravatar herbelin2003-05-20
* MAJ Simpl et ChangeGravatar herbelin2003-03-21
* Correction typo d'un but TautoGravatar herbelin2002-09-16
* documentation variante Subst (sans argument)Gravatar filliatr2002-09-16
* SubstGravatar filliatr2002-09-12
* MAJ syntaxe 'Hint Rewrite'Gravatar herbelin2002-09-09
* MAJ V7.3Gravatar herbelin2002-05-16
* doc Intuition et TautoGravatar courant2002-04-12
* Ajout Rename et PoseGravatar herbelin2002-04-11
* Quelques pr�cisions sur la convertibilit� et les tactiques Cbv/LazyGravatar herbelin2002-03-01
* Ajout ClearBody et Assert H:=tGravatar herbelin2001-12-23
* Ajout fonctionnalit� Intros Until de Injection, Discriminate et Simplify_eqGravatar herbelin2001-10-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 20:59:27 +0000