aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Options -strongly-constructive et -strongly-classicalGravatar herbelin2003-10-28
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
* Nouvelle fonction cherchant tous les noms d'un suffixe donneGravatar herbelin2003-10-21
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Fonctions utilesGravatar herbelin2003-09-23
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...Gravatar herbelin2003-09-12
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* errorGravatar herbelin2003-09-09
* Export process_module_bindings pour traducteurGravatar herbelin2003-09-02
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...Gravatar herbelin2003-06-10
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* code mortGravatar herbelin2003-06-10
* Extension renommageGravatar herbelin2003-05-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* CoqIde : but reset_modGravatar filliatr2003-05-19
* configure et make install s'occupent de CoqIde tout seulsGravatar filliatr2003-05-19
* but Require dans une SectionGravatar filliatr2003-05-19
* table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...Gravatar filliatr2003-05-15
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
* Orthographe anglaise - typosGravatar herbelin2003-05-13
* Orthographe anglaiseGravatar herbelin2003-05-13
* Corrige Bug (PR#290)Gravatar coq2003-05-05
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Affichage forcé des implicites contextuels si pas de contexte connuGravatar herbelin2003-04-10
* Bug init_functionGravatar herbelin2003-04-09
* Synchronisation séparée des implicites pour l'affichage du traducteur;Gravatar herbelin2003-04-09
* Correction Show ImplicitsGravatar herbelin2003-04-09
* Gestion synchronisation des Impargs.*_out et des Impargs._strict dans ImpargsGravatar herbelin2003-04-09
* Synchronisation avec resetGravatar herbelin2003-04-09
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Renommage unicite/unicity pour la v8Gravatar herbelin2003-04-07
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* ajout d'une fonction reset_modGravatar monate2003-03-26
* Ajout réaffichage SubClassGravatar herbelin2003-03-13
* *** empty log message ***Gravatar barras2003-03-12
* False dependencies in summaryGravatar coq2003-02-24
* Ajout du traducteurGravatar desmettr2003-02-05
* release 7.4; changement magic numberGravatar filliatr2003-02-03
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Deux p\'tits trucs ;)Gravatar coq2003-01-27