aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2006-09-28separation de RealFieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22doc du nouveau ringbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9158 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-20congruence doc updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9153 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-11Ajout eassumption indexherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9129 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-07Updating the doc about Function and cocourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9127 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Modification du manuel de référence: le flag evar pour cbv n'existe plus.notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Ajout thèse Cornesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16MAJ Rectutorial (P. Castéran)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9068 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28MAJ de la biblio du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9062 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-17MAJjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-12Documentation machine virtuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11MAJ doc/refmannotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Documentation de lazymatch et des extensions de idtac et failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9038 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Documentation Declare Implicit Tactic, Print Canonical Projections, ... + ↵herbelin
légère restructuration autour de Proof with et Hint Rewrite + maj crédits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07MAJ du manuel de référence (modules+fixpoints+pose proof)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9029 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-06Documentation Whelpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9028 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Ajout taclevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9019 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Documentation Print Ltac qualid; documentation du debugger de ltac.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9018 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Précisions sur l'Unicode reconnu; typo; ajout Example, Proposition, Corollary.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9013 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Mise à jour scopes prédéfinis et Tactic Notation pour tacticalsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9012 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Documentation 'external'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9011 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Doc Print Grammar patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9007 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Documentation or-patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9006 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Documentation or-patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Ajout cible refman-quick qui teste la compilation sans faire les index, toc ↵herbelin
et biblio git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9004 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Typo dans le manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' ↵herbelin
+ modifs diverses de la présentation des règles d'inférence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04MAJ du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03MAJ manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Nouveau paragraphe sur le polymorphisme de sorte des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8980 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Mention de coqide, proof general et pcoqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22updated documentation for my tactics (P. orbineaucorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13Changement du index.html généré dans refmannotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8953 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12Typo in replace doc. jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8951 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12Updating documentation of replace and correcting a typo in error message of ↵jforest
replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10ajout de la doc sur l'option -enable-geoproof de CoqIDEjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8945 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Commit doc Claudio Sacerdotiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8942 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Nouvelle MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09ajout de la doc de classical_right et leftjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8938 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09MAJ liste fichiers doc stdlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07petites corrections dans la doc de functional xxx. courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8915 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Nouveaux Parametres Inductifscpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8914 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07mise en texttt d'une commande.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Changements sur Functional xxx. Plus précis et plus exact.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8908 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06Ajout de précisions dans la doc de functional scheme et consort +courtieu
adaptation à la nouvelle version (syntaxe + sémantique). Reste Functional Scheme. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8905 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 17:24:05 +0000