aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2003-10-28Options -strongly-constructive et -strongly-classicalherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
2003-10-21Nouvelle fonction cherchant tous les noms d'un suffixe donneherbelin
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...herbelin
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-23Fonctions utilesherbelin
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-09errorherbelin
2003-09-02Export process_module_bindings pour traducteurherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...herbelin
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
2003-06-10code mortherbelin
2003-05-20Extension renommageherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-19CoqIde : but reset_modfilliatr
2003-05-19configure et make install s'occupent de CoqIde tout seulsfilliatr
2003-05-19but Require dans une Sectionfilliatr
2003-05-15table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...filliatr
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
2003-05-13Orthographe anglaise - typosherbelin
2003-05-13Orthographe anglaiseherbelin
2003-05-05Corrige Bug (PR#290)coq
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2003-04-10Affichage forcé des implicites contextuels si pas de contexte connuherbelin
2003-04-09Bug init_functionherbelin
2003-04-09Synchronisation séparée des implicites pour l'affichage du traducteur;herbelin
2003-04-09Correction Show Implicitsherbelin
2003-04-09Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargsherbelin
2003-04-09Synchronisation avec resetherbelin
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Renommage unicite/unicity pour la v8herbelin
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-26ajout d'une fonction reset_modmonate
2003-03-13Ajout réaffichage SubClassherbelin
2003-03-12*** empty log message ***barras
2003-02-24False dependencies in summarycoq
2003-02-05Ajout du traducteurdesmettr
2003-02-03release 7.4; changement magic numberfilliatr
2003-01-31Pour satisfaire ProofGeneralcoq
2003-01-27Deux p\'tits trucs ;)coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:01:57 +0000