aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-27Bug installation non localeherbelin
2000-12-25Bug discharge process_classherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert afi...herbelin
2000-12-19correction de bugs sur commit précédentherbelin
2000-12-19Découpage des différentes fonctionnalités de build_mutual et definition_st...herbelin
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
2000-12-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
2000-12-15 - suppression mind_extract_paramsfilliatr
2000-12-15Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...herbelin
2000-12-15Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...herbelin
2000-12-15Printermohring
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif d'u...herbelin
2000-12-14Amélioration message d'erreurherbelin
2000-12-14Raffinement erreur Wrong Predicateherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-12petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silentfilliatr
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-12-06Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...herbelin
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
2000-12-05Mini-nettoyage noms longsherbelin
2000-12-04caractere opaque des constantes repris en comptefilliatr
2000-11-30Changement de la syntaxe des options -I et -Rherbelin
2000-11-29Bug option -I et -R quand le répertoire est '..'herbelin
2000-11-29Bug option -I et -R quand le répertoire est '.'herbelin
2000-11-29Suppression cast inutileherbelin
2000-11-29Now AddRecPath and AddPath can be used with an As option to specify thesacerdot
2000-11-29load_path_entry structure simplified; field relative_subdir renamed to coq_di...sacerdot
2000-11-29Ajout d'une option d'alias à -Iherbelin
2000-11-29Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ch...herbelin
2000-11-28Remplacement des add_include par add_rec_include pour avoir le repertoire dan...herbelin
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-11-27Distinction local/globalherbelin
2000-11-27uniformisation messages d'erreurfilliatr
2000-11-27Prise en compte des définitions localesherbelin
2000-11-27Branchement des Local sur des SectionLocalDefherbelin
2000-11-26Prise en compte noms longs dans divers fonctions de Printherbelin
2000-11-26Remplacement de certains sp_of_id par des locateherbelin
2000-11-26sp au lieu de id dans END-SECTIONherbelin
2000-11-24Réorganisation autour de globalize_constrherbelin
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-24SearchPattern et SearchRewritefilliatr
2000-11-24- coqc: utilise le meilleur coq possiblefilliatr
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:38:50 +0000