aboutsummaryrefslogtreecommitdiff
path: root/contrib/field
AgeCommit message (Collapse)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
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-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Ajout fonctions syntaxe v8 pour contrib MapleModeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4457 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Système de renommage des noms de tactiques Ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4446 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Pour accomoder autant le printer v8 que v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4315 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Protection contre les types sans corps associéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4314 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4055 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Explicitation arguments de eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3914 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Mauvaise resolution conflit dans commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3859 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Légères simplifications code de Field; message d'erreur si pas égalitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01remplace == par = dans la tactique field pour que le debugger marche a ↵narboux
nouveau apres suppression de == par hugo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3837 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Fail 1 pour traverser le matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3832 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Plus de eqT; message Failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à ↵herbelin
la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 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-14MAJ syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3233 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-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-19Fix d'un bug sur le test des inversesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2542 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
Field term (nouveau) Injections dans l'interpreteur de tactiques Exportation de quelques entrees de grammaires Exportation de quelques fonctionnalites des definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Oubli d'un quoteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2318 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14oubli: changement de nil en nilTmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2192 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-14Changement de list en listT, cons en consT et app en appTmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2191 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-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Correction due au changement de semantique de Matchdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2049 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 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-07-10Ajout d'un Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1821 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27Reduction du terme preuve fourni par Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1813 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27Reduction tres significative du terme preuvedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1811 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1805 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
2001-04-24Suppression d'une partie de code commentedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1700 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20Ajout des entetesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1641 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 12:01:34 +0000