aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* distinction contexte et signatureGravatar filliatr2001-03-07
* plus de commentairesGravatar letouzey2001-03-06
* ocamlwebGravatar filliatr2001-03-05
* extraction termes (suite)Gravatar filliatr2001-03-05
* indentation codeGravatar filliatr2001-03-05
* De bizarres SR_pus_assoc au lieu de SR_plus_assocGravatar herbelin2001-03-01
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* debut extraction termes; pp lambdaGravatar filliatr2001-02-27
* ajout Vprop, Tprop et EpropGravatar filliatr2001-02-26
* extraction des types et des inductifsGravatar filliatr2001-02-22
* nouveau design ou le renommage sera fait a posterioriGravatar filliatr2001-02-21
* mise en place fichiers extractionGravatar filliatr2001-02-20
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Absolute URL for DTDs introducedGravatar sacerdot2001-02-13
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* mise en place extractionGravatar filliatr2001-02-06
* rétablissement patch ClaudioGravatar filliatr2001-02-05
* retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...Gravatar filliatr2001-02-02
* - coqc : option -imageGravatar filliatr2001-02-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Now Ring does not perform any more the same reduction twice.Gravatar sacerdot2001-01-12
* Comment fixedGravatar sacerdot2001-01-12
* Now reduction to normal form is done only when the term is notGravatar sacerdot2001-01-11
* Many unuseful rewritings are no more done by Ring.Gravatar sacerdot2001-01-11
* Mise a jour RbaseGravatar mohring2001-01-11
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Tactic Definition -> Meta DefinitionGravatar delahaye2001-01-09
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Scripts de correction d'uriGravatar herbelin2000-12-20
* MAJGravatar herbelin2000-12-20
* Non verbose par défautGravatar herbelin2000-12-20
* Bug sur commit précédentGravatar herbelin2000-12-14
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* type attribute added to PROD (for ForAll vs Pi rendering)Gravatar sacerdot2000-12-07
* COPYRIGHT file added; some comments changedGravatar sacerdot2000-12-07
* Bug identarg au lieu de qualidargGravatar herbelin2000-12-06
* Inner types are now reduced and arrows are created whenGravatar sacerdot2000-12-05
* LETIN now has a letintarget instead of a targetGravatar sacerdot2000-12-01
* cictypes.dtd changedGravatar sacerdot2000-12-01
* Used a force function to force stream evaluation only for aestaetics reasons.Gravatar sacerdot2000-11-30
* Identifier order in the inner-types file changed.Gravatar sacerdot2000-11-30
* Changement dans les noms longs (2eme)Gravatar herbelin2000-11-29
* Changement dans les noms longsGravatar herbelin2000-11-29
* Modifications due to the new As option in AddPath and AddRecPath.Gravatar sacerdot2000-11-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 05:02:59 +0000