aboutsummaryrefslogtreecommitdiff
path: root/doc/RefMan-tac.tex
AgeCommit message (Collapse)Author
2002-04-12doc Intuition et Tautocourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8277 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Ajout Rename et Poseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8276 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-01Quelques pr�cisions sur la convertibilit� et les tactiques Cbv/Lazyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8273 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-23Ajout ClearBody et Assert H:=therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8260 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Ajout fonctionnalit� Intros Until de Injection, Discriminate et Simplify_eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8245 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Adding documentation for a variant of Inversion, where a numeric argument,bertot
referring to the nth non-dependent product in the goal's conclusion, can be given instead of an hypothesis name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8244 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02MAJ Intro + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8239 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Diverses MAJ V7.1 autour des qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8221 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Documentation NewInduction, NewDestruct, LetTac, Assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8217 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Fourier, Reals,...mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8201 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajout d'une ref pour Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8197 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23Ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8196 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Changement de Zarith en ZArithmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8194 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-12Intros Pattern wildcardmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8189 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10MAJ decomposeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8182 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-08Revision Tauto, AutoRewrite + Ajout de Ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8172 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise a jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06mise a jour V7filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8169 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12Initial revisionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:25:05 +0000