aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-tac.tex
AgeCommit message (Expand)Author
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-07-06Documentation related to commit 9948: intropattern {A,B,C} for (A,(B,C))letouzey
2007-07-05documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/...letouzey
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
2007-06-07Ajout doc clear sans argumentherbelin
2007-05-11Made some places in the reference manual clearer. Correctedemakarov
2007-04-18Fixed some typos.glondu
2007-04-17Changed many refman/*.tex files. Put \label and \index commands that immediat...emakarov
2007-04-12Cleaned doc/common/title.tex file. Increased the space under headersemakarov
2007-04-05Mise en place d'un rafinement de compute. jforest
2007-03-13Correction bug #1439 (comportement de replace by)notin
2007-02-07doc de ring/field + option infinite -> completenessbarras
2007-02-01Report 9545 de 8.1 vers trunkherbelin
2007-01-31report de r9574: doc de fieldbarras
2007-01-26Explication du intros until nnotin
2006-12-23Doc for Combined Scheme.msozeau
2006-10-26MAJ crédits, fresh; documentation apply inherbelin
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
2006-10-04Doc injection asherbelin
2006-09-28separation de RealFieldbarras
2006-09-22doc du nouveau ringbarras
2006-09-20congruence doc updatecorbinea
2006-09-11Ajout eassumption indexherbelin
2006-09-07Updating the doc about Function and cocourtieu
2006-09-01Modification du manuel de référence: le flag evar pour cbv n'existe plus.notin
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-07-12Documentation machine virtuelleherbelin
2006-07-11MAJ doc/refmannotin
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...herbelin
2006-07-07MAJ du manuel de référence (modules+fixpoints+pose proof)notin
2006-07-04Typo dans le manuel de référencenotin
2006-07-04MAJ du manuel de référencenotin
2006-07-03MAJ manuel de référencenotin
2006-06-22updated documentation for my tactics (P. orbineaucorbinea
2006-06-12Typo in replace doc. jforest
2006-06-12Updating documentation of replace and correcting a typo in error message of r...jforest
2006-06-09ajout de la doc de classical_right et leftjnarboux
2006-06-07Changements sur Functional xxx. Plus précis et plus exact.courtieu
2006-06-06Ajout de précisions dans la doc de functional scheme et consort +courtieu
2006-06-05nouveaux parametrescpaulin
2006-04-28Continue l'écriture de la doc de "Function". Pas fini, manque:courtieu
2006-04-27Added a short doc for "Function". To be finished.courtieu
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin