aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Bug Identity CoercionGravatar herbelin2001-01-18
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Let doit etre utilise dans le mode de preuveGravatar delahaye2001-01-03
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Bug installation non localeGravatar herbelin2000-12-27
* Bug discharge process_classGravatar herbelin2000-12-25
* Un nom long pour les variables de section qui font classe ou coercion; réorg...Gravatar herbelin2000-12-25
* Import module force l'ouverture du module même s'il était déjà ouvert afi...Gravatar herbelin2000-12-20
* correction de bugs sur commit précédentGravatar herbelin2000-12-19
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* Amélioration message d'erreur mauvais prédicatGravatar herbelin2000-12-18
* Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteGravatar herbelin2000-12-16
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
* Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...Gravatar herbelin2000-12-15
* Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...Gravatar herbelin2000-12-15
* PrinterGravatar mohring2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* Amélioration message d'erreurGravatar herbelin2000-12-14
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silentGravatar filliatr2000-12-12
* Ajout erreur DoesNotOccurInGravatar herbelin2000-12-06
* Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...Gravatar herbelin2000-12-06
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
* Mini-nettoyage noms longsGravatar herbelin2000-12-05
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Changement de la syntaxe des options -I et -RGravatar herbelin2000-11-30
* Bug option -I et -R quand le répertoire est '..'Gravatar herbelin2000-11-29
* Bug option -I et -R quand le répertoire est '.'Gravatar herbelin2000-11-29
* Suppression cast inutileGravatar herbelin2000-11-29
* Now AddRecPath and AddPath can be used with an As option to specify theGravatar sacerdot2000-11-29
* load_path_entry structure simplified; field relative_subdir renamed to coq_di...Gravatar sacerdot2000-11-29
* Ajout d'une option d'alias à -IGravatar herbelin2000-11-29
* Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...Gravatar herbelin2000-11-29
* Remplacement des add_include par add_rec_include pour avoir le repertoire dan...Gravatar herbelin2000-11-28
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Distinction local/globalGravatar herbelin2000-11-27
* uniformisation messages d'erreurGravatar filliatr2000-11-27
* Prise en compte des définitions localesGravatar herbelin2000-11-27
* Branchement des Local sur des SectionLocalDefGravatar herbelin2000-11-27
* Prise en compte noms longs dans divers fonctions de PrintGravatar herbelin2000-11-26
* Remplacement de certains sp_of_id par des locateGravatar herbelin2000-11-26
* sp au lieu de id dans END-SECTIONGravatar herbelin2000-11-26
* Réorganisation autour de globalize_constrGravatar herbelin2000-11-24
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:58:53 +0000