aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2003-11-18Code mortherbelin
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-17Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)herbelin
2003-11-15Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarherbelin
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-11-14Compatibilite %Therbelin
2003-11-14Bug parsing castherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Suppression du "..." final !herbelin
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la biblio...herbelin
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...herbelin
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-12petits changements de syntaxebarras
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-09'as' avant 'using' dans 'destruct'herbelin
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
2003-11-06Added Instantiate ... incorbinea
2003-11-05Interpretation des entiers dans N (ex-entier), maj du module des positiveherbelin
2003-11-04En v8, une notation, c'est 2 regles et un niveauherbelin
2003-11-04Explicitation message d'erreur nombres negatifsherbelin
2003-11-03Compatibilite V7.4 pour le delimiteur de positiveherbelin
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 19:53:50 +0000