aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Mini-restructurationGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage coqlibGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7760 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage coqlibGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout booléens; nettoyageGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7756 85f007b7-540e-0410-9357-904b9bb8a0f7
* La distribution de Rocq/GRAPHS se fait via le serveur de contributions ↵Gravatar herbelin2005-12-29
| | | | | | utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7755 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaire mortGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement Pp.qs par Pptactic.qsnewGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Analyse des tests automatiques de compilation des contributionsGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement -no-vm par -vmGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7747 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mini-test d'extractionGravatar herbelin2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7743 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite correction nom QuantHypArgType suite suppression traducteurGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur; ↵Gravatar herbelin2005-12-26
| | | | | | changements collatéraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .v en ancienne syntaxeGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .v en ancienne syntaxeGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocaml 3.09Gravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction des noms v7 en noms v8Gravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation des noms de OmegaLemmas aux noms de Z; traduction des noms v7 de ↵Gravatar herbelin2005-12-25
| | | | | | Z de coq_omega.ml en noms v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction des noms v7 de Z en noms v8Gravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction des noms v7 de R en noms v8Gravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de -notop pour imposer l'absence de module toplevelGravatar herbelin2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7724 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de stratégie vis à vis du positionnement du module Top en mode ↵Gravatar herbelin2005-12-24
| | | | | | batch: si rien à compiler, on ouvre Top par défaut, pour l'éviter, il faut l'option -notop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de réparation du bug #1025: it seems like that a casted module ↵Gravatar herbelin2005-12-24
| | | | | | should only rely on the contents of its signature (i.e. with removal of the keep and special objects), doesn't it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7720 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7718 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Débranchement des parseurs de syntaxe v7Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ restructuration constrintern.mlGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification qu'un module est ouvert avant d'insérer une déclaration ↵Gravatar herbelin2005-12-23
| | | | | | nommée (peut arriver en mode -batch sans option -top) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction printer des Tactic NotationGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pr_module pour traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test printing of Tactic Notation which was broken until dec 2005Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7 (correction)Gravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contrepartie de la suppression des boites automatiques dans formatGravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7703 85f007b7-540e-0410-9357-904b9bb8a0f7
* option '-top dir' now works also in batch mode (2ème)Gravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
* option '-top dir' now works also in batch mode; it is even necessary to ↵Gravatar herbelin2005-12-22
| | | | | | ensure that loaded vernac definitions are defined inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7700 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-23 14:55:23 +0000