aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Précisions sur l'Unicode reconnu; typo; ajout Example, Proposition, Corollary.Gravatar herbelin2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour scopes prédéfinis et Tactic Notation pour tacticalsGravatar herbelin2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation 'external'Gravatar herbelin2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Doc Print Grammar patternGravatar herbelin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation or-patternGravatar herbelin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation or-patternGravatar herbelin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cible refman-quick qui teste la compilation sans faire les index, toc ↵Gravatar herbelin2006-07-04
| | | | | | et biblio git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans le manuel de référenceGravatar notin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' ↵Gravatar herbelin2006-07-04
| | | | | | + 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
* MAJ du manuel de référenceGravatar notin2006-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ manuel de référenceGravatar notin2006-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau paragraphe sur le polymorphisme de sorte des inductifsGravatar herbelin2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mention de coqide, proof general et pcoqGravatar herbelin2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
* updated documentation for my tactics (P. orbineauGravatar corbinea2006-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement du index.html généré dans refmanGravatar notin2006-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8953 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in replace doc. Gravatar jforest2006-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating documentation of replace and correcting a typo in error message of ↵Gravatar jforest2006-06-12
| | | | | | replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de la doc sur l'option -enable-geoproof de CoqIDEGravatar jnarboux2006-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit doc Claudio SacerdotiGravatar herbelin2006-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle MAJGravatar herbelin2006-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8941 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de la doc de classical_right et leftGravatar jnarboux2006-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8938 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ liste fichiers doc stdlibGravatar herbelin2006-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8937 85f007b7-540e-0410-9357-904b9bb8a0f7
* petites corrections dans la doc de functional xxx. Gravatar courtieu2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux Parametres InductifsGravatar cpaulin2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8914 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en texttt d'une commande.Gravatar courtieu2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changements sur Functional xxx. Plus précis et plus exact.Gravatar courtieu2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de précisions dans la doc de functional scheme et consort +Gravatar courtieu2006-06-06
| | | | | | | | 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
* Debut modif parametres inductifs CICGravatar cpaulin2006-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8902 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveaux parametresGravatar cpaulin2006-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8896 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update Program/subtac documentation.Gravatar msozeau2006-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support des modules dans CoqdocGravatar notin2006-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
* updating Function documentationGravatar jforest2006-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8825 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc du *in* de match/withGravatar barras2006-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction comportement clause _ du match goalGravatar herbelin2006-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵Gravatar notin2006-05-02
| | | | | | Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continue l'écriture de la doc de "Function". Pas fini, manque:Gravatar courtieu2006-04-28
| | | | | | | | - 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
* Ajout de la doc de l'option -stdout de coqdocGravatar notin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a short doc for "Function". To be finished.Gravatar courtieu2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enleve les commentairesGravatar cpaulin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 8.1-APPGravatar herbelin2006-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8707 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 8.1-APPGravatar herbelin2006-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de licence pour le Tutoriel de CoqGravatar notin2006-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8703 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
| | | | | | | | | | - 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
* MAJ Licence FAQGravatar herbelin2006-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug index addendum à cause mauvaise utilisation asection dans Helm.texGravatar herbelin2006-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite actualisation FAQGravatar herbelin2006-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
* - correction d'un bug dans coqdoc (multi_index)Gravatar notin2006-03-28
| | | | | | | - 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
* r8709@thot: notin | 2006-03-25 01:48:46 +0100Gravatar notin2006-03-25
| | | | | | | | - 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
* r8708@thot: notin | 2006-03-24 18:55:01 +0100Gravatar notin2006-03-25
| | | | | | | Correction d'un bug sur la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8662 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8637@thot: notin | 2006-03-14 16:00:49 +0100Gravatar notin2006-03-14
| | | | | | | | | - intégration de doc dans le Makefile principal - correction d'une incompatibilité avec Tetex 3.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 15:02:40 +0000