aboutsummaryrefslogtreecommitdiff
path: root/library/declare.ml
AgeCommit message (Expand)Author
2000-11-27Bug extract_instance en présence de défs localesherbelin
2000-11-27Prise en compte des let in dans les instances de globauxherbelin
2000-11-26Nettoyageherbelin
2000-11-26Prise en compte de noms absolus dans la nametab + nettoyageherbelin
2000-11-24Bug relocation des hypothèses quand les contextes de définitions et d'utili...herbelin
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-21implicites manuelsfilliatr
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ...filliatr
2000-11-20Nouveaux points d'accès pour les noms qualifiésherbelin
2000-11-15methode exportfilliatr
2000-11-09Renommage canonique SectionLocalDecl -> SectionLocalAssumherbelin
2000-11-08out_variable (Liboject.obj -> ...) distibgue de get_variablefilliatr
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Renommage canonique :herbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-03suppression de Fw pour les implicitesherbelin
2000-05-02construct_reference prend en compte aussi les variables du contextfilliatr
2000-04-28portage Omega (code seulement)filliatr
2000-04-21discharge des axiomesfilliatr
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-12modulesfilliatr
1999-12-10bug: enregistrement de vartab au lieu de csttabfilliatr
1999-12-10debug discharge et inductifsfilliatr
1999-12-09 - constantes avec recettesfilliatr
1999-12-08deplacement de Discharge dans toplevelfilliatr
1999-12-07correction bug construct_referencefilliatr
1999-12-06declarations eliminations / debuggae inductifs (debut)filliatr
1999-12-05add_leaf -> application methode cachefilliatr
1999-12-03bug make_strength reparefilliatr
1999-12-03 - global_reference traite des variablesfilliatr
1999-12-02Modifs suite à intégration de class.mlherbelin
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-01poursuite de Vernacentriesfilliatr
1999-12-01mise au point Declare et avancee dans Asttermfilliatr
1999-12-01make_strength / reset_libraryfilliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-29portage Astterm (partiellement)filliatr
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
1999-11-26prvectifilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 17:56:16 +0000