aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-03-14+ Debugging and cleaning functional principle generation tacticjforest
+ New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-14 r8637@thot: notin | 2006-03-14 16:00:49 +0100notin
- 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
2006-03-14 r8636@thot: notin | 2006-03-14 15:57:11 +0100notin
Correction de bugs de Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8625 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
arguments to a principle (like in map_ind). -Added nbranches and npredicates to elim_scheme, and made the elimc field optional. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8621 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-10cleaning jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-10Ajout Tutorial on recursive typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8619 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-08 r8620@thot: notin | 2006-03-08 11:44:16 +0100notin
Modifications diverses de Coqdoc: - modification du comportement par défaut de l'option --latex - ajout d'une option --stdout - réaménagement dans les sources (création de global.ml) - modification du parser de coqdoc pour regler les problèmes liés à  la syntaxe V8. - Correction du bug #1052 sur les commentaires en fin de ligne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-07Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain ↵jforest
is_empty in those versions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-07Modification des propriétés 'svn:ignore' pour correspondre aux .cvsignorenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8615 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03Liste des fichiers à ignorer lors du 'svn status'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8614 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03Suppression de la coupure entre base et addendum (quitte à le remettre si ↵herbelin
demandes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8613 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03Inutile en svnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8612 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03Propriété svn:ignoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8611 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-03Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8610 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-24Modification des propriétés des fichiers .tex (svn:executable)notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Uniformisation noms Library*.texherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8608 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Mise à jour des Makefile, ajout licences, corrections mineures suite àherbelin
restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Nettoyage de l'archive doc et restructuration avant intégration à l'archiveherbelin
principale de Coq et publication des sources (HH) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-27Ajout licence open publication � la doc (sous r�serve OK pour tutorial)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8605 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-10-14Pourquoi math goal parfois interditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8604 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-06plus de http://www.lri.fr/~letouzey/extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8603 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Updated new names of Local into Letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8602 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05suite commit pr�c�dentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8601 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05Copyright 2005herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8600 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-05Correction du bug de contraintes d'univers dans exType (mentionn� par ↵herbelin
Georges Gonthier) + diverses corrections de l'anglais US git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8599 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-07Ajout r�f�rence Luoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8598 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-07Ajout r�f�rences Alexandre Miquelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8597 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25Suppression cible all-ps-docs; ajout www/index.htmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8596 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05Correction sur signification induction doubleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8595 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-05Documentation v8 de 'set (id:=t) in ...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8594 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Ajout section sur lieursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8593 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-10Am�lioration doc bases de Hintsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8592 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-10Typos et orthographeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8591 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Documentation 'Focus num'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8590 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11Ajout pr�vention �chec en pr�sence de sous-typageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-08question pierre corrigenarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8588 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07ajout question Pierrenarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8587 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04minor ~ correction in coq'art urlkirchner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8586 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8585 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8584 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Probl�mes hevea + question evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8583 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Finalisation avant publicationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8582 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03bibtex et heveaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8581 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Pr�nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8580 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27Il faut 2 fois latex apr�s l'index (cf bug #793)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8579 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout RefMan 7.2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8578 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-19ajout question implicitnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8577 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 22:18:27 +0000