aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Collapse)AuthorAge
* separation de RealFieldGravatar barras2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
* doc du nouveau ringGravatar barras2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9158 85f007b7-540e-0410-9357-904b9bb8a0f7
* congruence doc updateGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout eassumption indexGravatar herbelin2006-09-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating the doc about Function and coGravatar courtieu2006-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification du manuel de référence: le flag evar pour cbv n'existe plus.Gravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9101 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout thèse CornesGravatar herbelin2006-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9089 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ biblioGravatar herbelin2006-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ biblioGravatar herbelin2006-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
| | | | | | | | | | | | 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
* MAJ de la biblio du manuel de référenceGravatar notin2006-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9062 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar jforest2006-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation machine virtuelleGravatar herbelin2006-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ doc/refmanGravatar notin2006-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation de lazymatch et des extensions de idtac et failGravatar herbelin2006-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation Declare Implicit Tactic, Print Canonical Projections, ... + ↵Gravatar herbelin2006-07-07
| | | | | | 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
* MAJ du manuel de référence (modules+fixpoints+pose proof)Gravatar notin2006-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation WhelpGravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation Print Ltac qualid; documentation du debugger de ltac.Gravatar herbelin2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9018 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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@9005 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
* 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
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-01 13:40:56 +0000