aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2003-11-01Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8herbelin
2003-11-01Il ne faut pas mettre le constrarg des tactiques au niveau lconstrherbelin
2003-11-01Extensibilite de la grammaires des patternsherbelin
2003-11-01Traduction des noms pour les refs de pr_glob_generic (via pr_global)herbelin
2003-11-01Utilisation de niveaux pour l'extensibilite de la grammaires des patternsherbelin
2003-11-01Extension de get_constr_entry et symbol_of_production pour gerer les extensio...herbelin
2003-11-01Heritage des notations v7 seulement si zero information v8herbelin
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-28Ajout de Print Visibilityherbelin
2003-10-23Saut de ligne avant les infos non logiques de print_aboutherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-23Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionherbelin
2003-10-23Independance de grammar.cmo vis a vis de Searchherbelin
2003-10-22Suppression dependance formelle en Vernacexprherbelin
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...herbelin
2003-10-21Extension de Locateherbelin
2003-10-17On n'autorise plus les niveaux doubles L/R en v8herbelin
2003-10-17Bug mot-cle TYPESherbelin
2003-10-17Traduction des idents aussi dans le printer generique des tactiquesherbelin
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-16lettac -> setbarras
2003-10-16Bug Searchherbelin
2003-10-15Mise en conformite return_type en fonction de la docherbelin
2003-10-14Changement 'as notation' en 'where notation'herbelin
2003-10-13Ameliration affichage inductifsherbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-11Ajout fnl() dans Aboutherbelin
2003-10-11mise a jour nouvelle syntaxebarras
2003-10-10Suppression Grammar/Syntaxherbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-10-10Cablage en dur de inversionherbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-09Compatibilite ocaml 3.06 et 3.07herbelin
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...herbelin
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop com...herbelin
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
2003-10-02Hypothesis mot-cleherbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-26Bug aboutherbelin
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
2003-09-26Ajout 'About'herbelin
2003-09-26Re-possibilite changement chaine infixe en passant v7 a v8herbelin
2003-09-24Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 04:57:27 +0000