aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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
2006-06-06Debut modif parametres inductifs CICcpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8902 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-05nouveaux parametrescpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8896 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-01Update Program/subtac documentation.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8890 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Support des modules dans Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-17updating Function documentationjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8825 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05doc du *in* de match/withbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8796 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05Correction comportement clause _ du match goalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8790 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵notin
Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Continue l'écriture de la doc de "Function". Pas fini, manque:courtieu
- relecture par YB et JF - adaptation de la partie functional induction - écriture de la partie functional inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8770 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Ajout de la doc de l'option -stdout de coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Added a short doc for "Function". To be finished.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8743 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14Enleve les commentairescpaulin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-13MAJ 8.1-APPherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8707 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-13MAJ 8.1-APPherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8706 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-12Changement de licence pour le Tutoriel de Coqnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8703 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-07- Documentation of the Program tactics.msozeau
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05MAJ Licence FAQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-04Bug index addendum à cause mauvaise utilisation asection dans Helm.texherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8678 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-31Petite actualisation FAQherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28- correction d'un bug dans coqdoc (multi_index)notin
- modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8709@thot: notin | 2006-03-25 01:48:46 +0100notin
- Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 10:09:31 +0000