aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* reparation des $Gravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
| | | | | | | | | | | | | pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Debugging and cleaning functional principle generation tacticGravatar jforest2006-03-14
| | | | | | | | | + New functional induction now calls induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8627 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
* r8636@thot: notin | 2006-03-14 15:57:11 +0100Gravatar notin2006-03-14
| | | | | | | Correction de bugs de Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8625 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | 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
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
| | | | | | | | | | 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
* MAJGravatar herbelin2006-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8621 85f007b7-540e-0410-9357-904b9bb8a0f7
* cleaning Gravatar jforest2006-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Tutorial on recursive typesGravatar herbelin2006-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8619 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8623@thot: notin | 2006-03-08 12:40:57 +0100Gravatar notin2006-03-08
| | | | | | | 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
* r8620@thot: notin | 2006-03-08 11:44:16 +0100Gravatar notin2006-03-08
| | | | | | | | | | | | | | 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
* Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain ↵Gravatar jforest2006-03-07
| | | | | | is_empty in those versions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés 'svn:ignore' pour correspondre aux .cvsignoreGravatar notin2006-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Liste des fichiers à ignorer lors du 'svn status'Gravatar herbelin2006-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la coupure entre base et addendum (quitte à le remettre si ↵Gravatar herbelin2006-03-03
| | | | | | demandes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inutile en svnGravatar herbelin2006-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8612 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propriété svn:ignoreGravatar herbelin2006-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8611 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2006-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés des fichiers .tex (svn:executable)Gravatar notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty2006-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation noms Library*.texGravatar herbelin2006-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des Makefile, ajout licences, corrections mineures suite àGravatar herbelin2006-02-23
| | | | | | | restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23
| | | | | | | 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
* Ajout licence open publication � la doc (sous r�serve OK pour tutorial)Gravatar herbelin2006-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pourquoi math goal parfois interditGravatar herbelin2005-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8604 85f007b7-540e-0410-9357-904b9bb8a0f7
* plus de http://www.lri.fr/~letouzey/extractionGravatar letouzey2005-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated new names of Local into LetGravatar herbelin2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8602 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite commit pr�c�dentGravatar herbelin2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copyright 2005Gravatar herbelin2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug de contraintes d'univers dans exType (mentionn� par ↵Gravatar herbelin2005-05-05
| | | | | | 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
* Ajout r�f�rence LuoGravatar herbelin2005-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout r�f�rences Alexandre MiquelGravatar herbelin2005-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression cible all-ps-docs; ajout www/index.htmlGravatar herbelin2005-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction sur signification induction doubleGravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation v8 de 'set (id:=t) in ...'Gravatar herbelin2004-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout section sur lieursGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Am�lioration doc bases de HintsGravatar herbelin2004-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8592 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typos et orthographeGravatar herbelin2004-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation 'Focus num'Gravatar herbelin2004-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout pr�vention �chec en pr�sence de sous-typageGravatar herbelin2004-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8589 85f007b7-540e-0410-9357-904b9bb8a0f7
* question pierre corrigeGravatar narboux2004-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8588 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout question PierreGravatar narboux2004-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8587 85f007b7-540e-0410-9357-904b9bb8a0f7
* minor ~ correction in coq'art urlGravatar kirchner2004-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8586 85f007b7-540e-0410-9357-904b9bb8a0f7
* OublisGravatar herbelin2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8585 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Probl�mes hevea + question evarsGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalisation avant publicationGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8582 85f007b7-540e-0410-9357-904b9bb8a0f7
* bibtex et heveaGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pr�nomsGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Il faut 2 fois latex apr�s l'index (cf bug #793)Gravatar herbelin2004-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8579 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:09:08 +0000