aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
...
* Mise en place d'un nouveau Destruct sur le modèle du nouvel InductionGravatar herbelin2001-08-05
* Changements dans le traitement des qualid'sGravatar delahaye2001-07-19
* modifs de preuves (plus simples)Gravatar mayero2001-07-19
* reparation regles pour parsing Coercion LocalGravatar mohring2001-07-13
* ajout Show Intro(s)Gravatar letouzey2001-07-04
* Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...Gravatar herbelin2001-07-02
* Ajout glob_eq{,T}Gravatar herbelin2001-07-02
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...Gravatar herbelin2001-06-25
* Extension des parametres de Clear + InstGravatar delahaye2001-06-19
* Interpretation MetaId + Progress + InstGravatar delahaye2001-06-18
* Reparation d'un bug d'affichage. Les let destructurants, if, et vieux CaseGravatar clrenard2001-06-11
* Fix de quelques bugs syntaxiques de LtacGravatar delahaye2001-06-11
* Retablissement de minicoqGravatar coq2001-05-29
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Pretty -> PrettypGravatar filliatr2001-05-28
* Changement de la structure des points fixesGravatar barras2001-05-03
* message d'erreur pour rattrapper l'anomalie avec SQUASHGravatar barras2001-04-25
* Amelioration affichageGravatar herbelin2001-04-25
* Messages d'erreur CasesGravatar herbelin2001-04-24
* Les clauses de Rec doivent prendre des tactic_atom'sGravatar delahaye2001-04-24
* un warning pas beau supprimméGravatar filliatr2001-04-23
* Petit menageGravatar delahaye2001-04-20
* *** empty log message ***Gravatar mayero2001-04-19
* Essais dans LtacGravatar delahaye2001-04-19
* Bug affichage d'implicites pour les vars lieesGravatar herbelin2001-04-15
* Non parenthesage des applications de tactiquesGravatar delahaye2001-04-14
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* Modified searchPattern. Before this correction, constructors were overlooked,Gravatar bertot2001-04-10
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
* nettoyage d'entrees de grammaires inutilesGravatar courant2001-04-09
* branchement extraction en standard (pas de Require)Gravatar filliatr2001-04-09
* bug Print Proof; usage coqtop/coqcGravatar filliatr2001-04-06
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* Add a flag to avoid sending too many warnings when reloading syntax filesGravatar bertot2001-04-04
* adding entry points for the arguments of the Comment command.Gravatar bertot2001-04-04
* Adding A command for comments, this makes it possible to have structuredGravatar bertot2001-04-04
* The function filter_by_module, that was previously exported was not theGravatar bertot2001-04-03
* Export a function (build_inductive) that is used in the graphical interface.Gravatar bertot2001-04-03
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* amelioration de la structure des universGravatar barras2001-03-28
* amelioration de la consommation memoire de la conversion en eta-expansantGravatar barras2001-03-23
* Bug MUTCASE au lieu CASEGravatar herbelin2001-03-22
* entetesGravatar filliatr2001-03-15
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Bug affichage coercionsGravatar herbelin2001-02-16
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Tentative d'amélioration affichage decls localesGravatar herbelin2001-02-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:34:57 +0000