aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Double bug de interp_modifiers anciennement caché par un troisième que les ↵Gravatar herbelin2005-12-22
| | | | | | nouveaux warnings de ocaml 3.09 avaient révélé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bugs commit précédentGravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; ajouts tests modulesGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7692 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7690 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ syntaxe v7 avant activation en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activation du test de Refine en v7 pour mémoire avant passage à la v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Anciennement déplacé dans 'output'Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7687 85f007b7-540e-0410-9357-904b9bb8a0f7
* cf ltac4.vGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7686 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Divers; restructuration des points d'entrée de ConstrinternGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'information que certaines tactiques attendent un type ↵Gravatar herbelin2005-12-21
| | | | | | (utile pour coercions et interpretation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de ↵Gravatar herbelin2005-12-21
| | | | | | tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation: extension de la suppression d'un casts dans collapse_app à ↵Gravatar herbelin2005-12-21
| | | | | | la suppression de cascades de casts (utile pour le 4CT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7680 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans ↵Gravatar herbelin2005-12-20
| | | | | | metasyntax.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7677 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la mise en boite automatique si format utilisateurGravatar herbelin2005-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7670 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7668 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'option -no-vm laisse la place à une option -vmGravatar herbelin2005-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7667 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7664 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵Gravatar herbelin2005-12-17
| | | | | | (suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵Gravatar herbelin2005-12-17
| | | | | | et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-16 00:44:33 +0000