aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Extension de l'utilisation de contradictionGravatar herbelin2003-10-19
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* Ground update + Linear removalGravatar corbinea2003-10-16
* Branchement sur RIneqGravatar herbelin2003-10-16
* Ground update changing left-arrow-arrow rule.Gravatar corbinea2003-10-13
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
* Cablage en dur de inversionGravatar herbelin2003-10-10
* show_subgoals dans PfeditGravatar herbelin2003-10-10
* Affichage des buts par Pfedit pour utilisation par les tactiquesGravatar herbelin2003-10-10
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Compatibilite V7 des noms d'hypothesesGravatar herbelin2003-10-07
* pour ocamlwebGravatar letouzey2003-10-06
* distinguer interp_cs et interp_setcsGravatar letouzey2003-10-06
* Cacher les .v8Gravatar herbelin2003-10-03
* Plus de nom commencant par '_' en V8Gravatar herbelin2003-10-02
* Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'Gravatar herbelin2003-09-30
* oupsGravatar letouzey2003-09-28
* 2 pbs de plus réglés concernant Setoid Ring:Gravatar letouzey2003-09-28
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
* Changement de l'afficheur pour que les variables liées aient un nom indépen...Gravatar herbelin2003-09-23
* Ajout fonctions syntaxe v8 pour contrib MapleModeGravatar herbelin2003-09-23
* commit accidentel d'une bidouilleGravatar letouzey2003-09-22
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* Système de renommage des noms de tactiques LtacGravatar herbelin2003-09-22
* suite (et fin) reparation Setoid RingGravatar letouzey2003-09-22
* tentative de rafraichissement de Setoid RingGravatar letouzey2003-09-22
* Passage à la V8 par défautGravatar herbelin2003-09-22
* Changement de la politique de V8only: V8only tout seul signifieGravatar herbelin2003-09-21
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
* parsingGravatar herbelin2003-09-19
* Indépendance vis à vis de DeclareGravatar herbelin2003-09-12
* Ajout 'Print Scopes' et 'Bind Scope with classes'Gravatar herbelin2003-09-12
* Simplification vis a vis de DeclareGravatar herbelin2003-09-12
* Branchement constant sur CoqlibGravatar herbelin2003-09-12
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
* Mise en place possibilité de définitions locales dans les paramètres des r...Gravatar herbelin2003-09-06
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
* Mise en place possibilité de définitions locales dans les paramètres des i...Gravatar herbelin2003-09-06
* Pour accomoder autant le printer v8 que v7Gravatar herbelin2003-09-06
* Protection contre les types sans corps associéGravatar herbelin2003-09-06
* bug dans calcul nb d'occurrencesGravatar letouzey2003-09-05
* correction d'un stack overflow possible (PR#320)Gravatar letouzey2003-08-28
* Traducteur de correctnessGravatar herbelin2003-08-14
* code mortGravatar herbelin2003-08-14
* Traduction mlnamesGravatar herbelin2003-08-14