aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4448 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4390 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4337 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4325 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-03*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4297 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Mémo nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4259 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16prettyprint des constr_substituted + un wrapping de prglobal pour qu'il ↵letouzey
n'echoue jamais lors d'un débug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3928 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Ajout translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3845 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-18Ajout translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3779 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-07Petites modifs de mes super-Makefiles ;)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3749 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Ajout pptacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3531 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-05Ajout affichage fconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3382 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout interpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3263 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-04ajout d'un printer pour les global_referenceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3204 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Cool dev/Makefile'scoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3054 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-13Ajout contribs manquantesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3005 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13AutoRewrite substitutive...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2965 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Petites corrections ici et lacoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2787 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-20Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceddr
qu'il entre en conflit avec le module Errors ajouté dans OCaml courant (future version OCaml 3.05). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2489 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-15petits changements cosmetiques sur les tactiquesbarras
+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07suppression du retour chariot a la fin de print_pure_constrbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2459 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2382 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Pour les développeurs extérieursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2339 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Réorganisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2331 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Pour les développeurs extérieursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2330 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJ V7.2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2329 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1812 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Retablissement de minicoqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10ajout d'un afficher de contexte et d'une fonction constbody_of_stringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1739 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:00:00 +0000