aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* 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
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Now also inner-types are exported.Gravatar sacerdot2000-11-29
* Code clean-up due to the new usage of longer names in Coq.Gravatar sacerdot2000-11-28
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Elimination du 'Gravatar delahaye2000-11-28
* Many improvements. Xml contrib retached to the V7.Gravatar sacerdot2000-11-27
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Simplification de l'accès aux globauxGravatar herbelin2000-11-23
* id_of_global devient sp_of_globalGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Changed the semantics of AddRecPath.Gravatar sacerdot2000-11-15
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* nouveau load pathGravatar filliatr2000-11-08
* First version with out_variable used. Exports all the standard libraryGravatar sacerdot2000-11-08
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Correction sur commit errone de la version 1.3Gravatar herbelin2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* Few OCaml files in contrib/xmlGravatar sacerdot2000-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:55:31 +0000