aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵herbelin
(suite): correction des dépendances (et notamment non-dépendance en unix.cma) pour la création de printers.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7787 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵herbelin
(débranchées depuis mars 01) + affichage plus concis des locations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7785 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Achèvement du commit incomplet de la révision 1.110 (cvs log ↵herbelin
toplevel/metasyntax.ml) sur les formats de notations récursives + ajout de cassure par défaut en cas de notation récursive sans séparateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7783 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7781 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03Modification pour que l'ordre des éléments respecte l'ordre dans lequel ↵herbelin
ils ont été déclarés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7780 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03Redéclaration de la notation à l'import pour être cohérent avec ↵herbelin
l'activation à l'import des notations qui ne sont pas des définitions syntaxiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7779 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7775 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-02Affichage de 'O' (lettre) comme '0' (chiffre)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7772 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7770 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7768 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Application du souhait de transparence de well_founded_ltof (#1007)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7766 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Test bug #1025herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7765 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Correction dépendance g_prim.ml4/q_coqast.ml4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7763 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵herbelin
de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Mini-restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Nettoyage coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7760 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Nettoyage coqlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7759 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout booléens; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7756 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-29La distribution de Rocq/GRAPHS se fait via le serveur de contributions ↵herbelin
utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7755 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7753 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Commentaire mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7752 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7751 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Analyse des tests automatiques de compilation des contributionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7749 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Remplacement -no-vm par -vmherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7747 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7745 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-27Autres suppressions de composantes du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-27Mini-test d'extractionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7743 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7741 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
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
2005-12-26Petite correction nom QuantHypArgType suite suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Achèvement suppression traducteur dans contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur; ↵herbelin
changements collatéraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(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
2005-12-26Suppression des fichiers .v en ancienne syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7735 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(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
2005-12-26Suppression des fichiers .v en ancienne syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(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
2005-12-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7730 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Compatibilité ocaml 3.09herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7729 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Traduction des noms v7 en noms v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7728 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Adaptation des noms de OmegaLemmas aux noms de Z; traduction des noms v7 de ↵herbelin
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
2005-12-25Traduction des noms v7 de Z en noms v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7726 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Traduction des noms v7 de R en noms v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7725 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-25Utilisation de -notop pour imposer l'absence de module toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7724 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7722 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-24Changement de stratégie vis à vis du positionnement du module Top en mode ↵herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 10:42:34 +0000