aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2001-08-06Nouvelle entrée ident_or_numargherbelin
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
2001-07-19Changements dans le traitement des qualid'sdelahaye
2001-07-19modifs de preuves (plus simples)mayero
2001-07-13reparation regles pour parsing Coercion Localmohring
2001-07-04ajout Show Intro(s)letouzey
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Ajout glob_eq{,T}herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
2001-05-29Retablissement de minicoqcoq
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-28Pretty -> Prettypfilliatr
2001-05-03Changement de la structure des points fixesbarras
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
2001-04-25Amelioration affichageherbelin
2001-04-24Messages d'erreur Casesherbelin
2001-04-24Les clauses de Rec doivent prendre des tactic_atom'sdelahaye
2001-04-23un warning pas beau supprimméfilliatr
2001-04-20Petit menagedelahaye
2001-04-19*** empty log message ***mayero
2001-04-19Essais dans Ltacdelahaye
2001-04-15Bug affichage d'implicites pour les vars lieesherbelin
2001-04-14Non parenthesage des applications de tactiquesdelahaye
2001-04-12Ajout de _ dans les patterns d'intromohring
2001-04-10Modified searchPattern. Before this correction, constructors were overlooked,bertot
2001-04-09Uniformisation des 'Save def_tok id'herbelin
2001-04-09nettoyage d'entrees de grammaires inutilescourant
2001-04-09branchement extraction en standard (pas de Require)filliatr
2001-04-06bug Print Proof; usage coqtop/coqcfilliatr
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...filliatr
2001-04-04Add a flag to avoid sending too many warnings when reloading syntax filesbertot
2001-04-04adding entry points for the arguments of the Comment command.bertot
2001-04-04Adding A command for comments, this makes it possible to have structuredbertot
2001-04-03The function filter_by_module, that was previously exported was not thebertot
2001-04-03Export a function (build_inductive) that is used in the graphical interface.bertot
2001-03-30branchement extraction (bytecode seulement)filliatr
2001-03-28amelioration de la structure des universbarras
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
2001-03-22Bug MUTCASE au lieu CASEherbelin
2001-03-15entetesfilliatr
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16Bug affichage coercionsherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 21:48:24 +0000