aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
* Correction bug #1333 (test non récursivité des dépendances en d'autresGravatar herbelin2007-01-24
* Merge with Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)Gravatar herbelin2006-12-09
* Changement du magic numberGravatar notin2006-11-06
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
* Indentation + svnpropGravatar notin2006-09-12
* Indentation + typoGravatar notin2006-09-01
* Un peu de delta-réduction...Gravatar herbelin2006-08-31
* Correction du bug #1170: les options synchronisées déclarées dans une sect...Gravatar notin2006-07-27
* Nombre magique pour la 8.1betaGravatar herbelin2006-07-13
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Ajout chop_dirpathGravatar herbelin2006-04-27
* Changement anomaly en failwith dans out_name pour utilisation par map_succeedGravatar herbelin2006-04-24
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* Ajout array_fold_map', list_fold_map' et list_remove_firstGravatar herbelin2006-03-29
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Ajout syntaxe concrète Proposition, synonyme de LemmaGravatar herbelin2006-01-29
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* - Ajout syntaxe concrète Property/Corollary, synonymes de LemmaGravatar herbelin2006-01-28
* *** empty log message ***Gravatar barras2006-01-20
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Tentative de réparation du bug #1025: it seems like that a casted module sho...Gravatar herbelin2005-12-24
* Vérification qu'un module est ouvert avant d'insérer une déclaration nommÃ...Gravatar herbelin2005-12-23
* Changement des named_contextGravatar gregoire2005-12-02
* Fonctionnalisation du cache 'compunit' pour réparer correctement le bug #103...Gravatar herbelin2005-11-26
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Conformité au principe du nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
* Types inductifs parametriquesGravatar mohring2005-11-02
* Correction bug #1030 (conséquence du commit 1.84 sur le discharge: add_froze...Gravatar herbelin2005-11-01
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...Gravatar herbelin2005-02-18