aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml
Commit message (Expand)AuthorAge
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Petit netoyage dans libGravatar coq2002-12-19
* simplification de solve_subgoal: n'utilise plus frontierGravatar barras2002-12-19
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration de la branche mowgliGravatar herbelin2002-11-05
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Suppression automatique du corps des définitions locales opaques dansGravatar herbelin2002-08-17
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* OrthographeGravatar herbelin2002-01-11
* reparation du make depend et du .dependGravatar letouzey2001-12-19
* Mise en place d'une méthode directe pour indiquer le type des déclarations ...Gravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Report des modifs de ClaudioGravatar herbelin2001-09-20
* ParsingGravatar herbelin2001-08-10
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* application patch ClaudioGravatar filliatr2001-05-11
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* 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
* Absolute URL for DTDs introducedGravatar sacerdot2001-02-13
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* 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