aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-09-08Meilleur anglais (cf #841)herbelin
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-08-26Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...herbelin
2004-08-23Précisions message d'erreurherbelin
2004-07-29Distinction location ocaml 3.08 ou pas (suite)herbelin
2004-07-29Distinction location ocaml 3.08 ou pasherbelin
2004-07-28Bug tactique fixherbelin
2004-07-23"Print Setoids" command added.sacerdot
2004-07-20Abstraction vis à vis de dummy_locherbelin
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
2004-07-16Suppression quotifyherbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Branchement sur Util.loc et abstraction vis a vis de dummy_locherbelin
2004-07-16Abstraction vis a vis de dummy_locherbelin
2004-07-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-29efficacite du lexeurfilliatr
2004-06-28more evar stuffcorbinea
2004-06-17Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsherbelin
2004-06-03Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)herbelin
2004-06-02Affichage de l'opacité dans Print et Aboutherbelin
2004-05-27Bug affichage ClearBodyherbelin
2004-05-14Bug syntaxe AddPathherbelin
2004-03-26Ajout entree pour exporter les commentaires en mode -xmlherbelin
2004-03-25Code mortherbelin
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...herbelin
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...herbelin
2004-03-17Parsing des V8Notation avec motif recursif en v7herbelin
2004-03-17Utilisation de '..' pour la notation concrete des motifs recursifs de filtrageherbelin
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications au...herbelin
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-03-03Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'herbelin
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...herbelin
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...herbelin
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...herbelin
2004-03-02Correction oubli du cas pas d'arguments implicites du toutherbelin
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte des...herbelin
2004-02-28Expansion du type par nécessité dans le cas d'affichage d'implicitesherbelin
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
2004-02-21Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...herbelin
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-02-17Ajout de lconstr, constr et binder_constr dans Print Grammar constrherbelin
2004-02-16export the general function for getting information from the environmentbertot
2004-02-13Uniformisation du comportement de Notation et Reserved Notationherbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2004-01-29Suppression de 'Print.' en v8herbelin
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...herbelin
2004-01-27Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 06:40:45 +0000