aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2002-11-20Correction des priorités des TOMATCHherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3259 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-20Ajout option_fold_left2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3258 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-19Autoriser les abbreviations de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3257 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18remaniement de test_extraction.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3256 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3255 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Allègement du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3254 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Analyse plus fine des occurrences rigidesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3253 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans laherbelin
contrib Suresnes/MiniC]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3252 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Definition et proprietes de l'integrale de Riemanndesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3251 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Proprietes des fonctions en escalierdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3250 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3249 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-17Problème avec le choix d'introduire une indirection vers un rawconstr pourherbelin
les extensions de grammaire par Grammar; pose p.ex. problème pour la résolution des implicites. Pour l'instant, une rustine pour contourner le problème git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3248 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-16Complétion du commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3247 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3246 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ↵herbelin
(càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15maj apres reparation d'un bug coqdepletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3244 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15Bug de coqdep qui n'acceptait pas les fichiers DOS (cf Binome.v)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3243 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15Bug factorisation grammaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3242 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3241 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Compatibilité avec les << >> dans la très ancienne syntaxe des actionsherbelin
de Grammar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3240 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Bug factorisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3239 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Restauration échappement MLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3238 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Re-ajout constrInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14bugsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3236 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:00:12 +0000