aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-12-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3358 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Remplacement Grammar par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3357 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02MAJ sur MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3356 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Associativité de constr9 et lconst à RIGHTA qui est le plus courantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3354 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3353 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ↵herbelin
uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...); Diverses améliorations affichage et parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3352 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3351 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_exprherbelin
(globalisation uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...). Diverses améliorations affichage et parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3350 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3349 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02On force l'associativité pour les entrées sans niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3348 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-01Synchro level (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3347 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3346 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-292 bugs: 1) projections pas renommées 2) mutual fixpoints a l'enversletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3345 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Raffinement syntaxe Infixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3344 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Utilisation de Snext pour gérer les symboles non associatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3343 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3342 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Synchro de la table des niveaux avec les sectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3341 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29constr9 et lconstr NONA pour une meilleur extensibilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3340 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29Re-échappement des \ et " dans les token stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3339 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3338 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-29cosmetiqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3337 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Remaniement du pp, suite: vers un renommage modulaire correcteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3336 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Quelques Set et Map spécialisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3335 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Affinement de la gestion des niveaux toujours; type ETBigintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3334 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Essai d'une autre syntaxe pour la dlimitation des scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3333 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Ajout d'une entre Prim.bigintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3332 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Court-circuit de g_zsyntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3331 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Bug exceptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3330 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Court-circuit de g_zsyntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3329 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Simplificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3328 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Essai de suppression du caractere d'echappement des stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3327 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Oubliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3326 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28suite et fin des records avec ocamlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3325 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28 bug pp letin + un inductif constant n'est pas un recordletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3324 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Re-Oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3323 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3322 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Reorganisation du pretty-print:letouzey
- Dfix sans rename_global - question du renommage - code cleanup (plein) Encore a finir: bug modules/qualification et syntax records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3321 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28A usage cosmetiqueletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3320 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28typo ?letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3319 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3318 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3317 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Affinement encoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3316 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Plus de précisionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3315 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Affinement de la gestion des niveauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3314 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27cond_pos -> cond_positivity pour cause de conflit avec posreal...desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3313 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3312 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Réorganisation de la librairie des réelsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Ajout répertoire interpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3310 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-27Extraction des Record, suiteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3309 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-21 23:44:26 +0000