aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-11-27Extraction des Record, suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3309 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Retour sur associativité à droite de * pour compatibilité de prodherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3308 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Correction sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3307 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3306 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Remplacement Grammar/Syntax par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3305 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Remplacement des Grammar et des [| |] par des notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3304 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26pseudo-parser ocamlyacc de la nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3303 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Ne pas cacher les Metas d'une notations, ils peuvent être liant dansherbelin
les filtrage de ltac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3302 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Options make coqlight/ make install-coqlight pour les impatients...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3301 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3300 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Option pour compiler une version 'light' des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3299 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26MAJdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3298 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Theorie 'light' des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3297 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3296 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Réaffichage des Syntactic Definition (printer constr_expr).herbelin
Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5herbelin
qui est le niveau des relations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3294 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Affichage nom le plus court pour Syntactic Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3293 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Plus d'indication pour le gestionnaire de niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3292 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Correction affichage entiers en cas d'échecherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3291 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3290 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Ajout list_map_assocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3289 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Bug niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3288 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26debut de support des records camlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3287 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3286 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25correction bug n°191letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3285 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25cleanup table.ml + erreur si Extraction Inline sous sectionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3284 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Syntaxe delimiteursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3283 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Retablissement Syntactic Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3282 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25MAJ delimiters et niveaux d'associativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3281 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Z dans les patterns via les scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3280 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Rétablissement affichage des entiers de natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3279 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Retablissement SynDef Value/Errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3278 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3277 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3276 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Retour sur le choix des delimiteursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3275 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3274 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3273 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Rétablissement printer via astherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3272 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3271 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵herbelin
améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Généralisation de l'utilisation de Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3269 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Installation des printers de nombres pour constr_exprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3268 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout Refmapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3266 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout option_consherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3265 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Ajout zeroherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3264 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-24Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3262 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Les parenthèses de la notation '(n)' maintemant mises par ML pour un ↵herbelin
meilleur affichage des entiers dans le scope nat_scope git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3261 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Introduction d'un constructeur ARROW; rétablissement priorités desherbelin
arguments de APPTAIL (autre méthode dans g_constr.ml4 pour gérer le conflit entre "(f 3+4)" et "(f 3!x)") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3260 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:50:37 +0000