aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
Commit message (Expand)AuthorAge
...
* Prise en compte des let in dans les instances de globauxGravatar herbelin2000-11-27
* NettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametab + nettoyageGravatar herbelin2000-11-26
* Bug relocation des hypothèses quand les contextes de définitions et d'utili...Gravatar herbelin2000-11-24
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* implicites manuelsGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Nouveaux points d'accès pour les noms qualifiésGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* suppression de Fw pour les implicitesGravatar herbelin2000-05-03
* construct_reference prend en compte aussi les variables du contextGravatar filliatr2000-05-02
* portage Omega (code seulement)Gravatar filliatr2000-04-28
* discharge des axiomesGravatar filliatr2000-04-21
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* modulesGravatar filliatr1999-12-12
* bug: enregistrement de vartab au lieu de csttabGravatar filliatr1999-12-10
* debug discharge et inductifsGravatar filliatr1999-12-10
* - constantes avec recettesGravatar filliatr1999-12-09
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* correction bug construct_referenceGravatar filliatr1999-12-07
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* add_leaf -> application methode cacheGravatar filliatr1999-12-05
* bug make_strength repareGravatar filliatr1999-12-03
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Modifs suite à intégration de class.mlGravatar herbelin1999-12-02
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* poursuite de VernacentriesGravatar filliatr1999-12-01
* mise au point Declare et avancee dans AsttermGravatar filliatr1999-12-01
* make_strength / reset_libraryGravatar filliatr1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage Astterm (partiellement)Gravatar filliatr1999-11-29
* module Classops; ajout de fonctions dans Declare en consequenceGravatar filliatr1999-11-26
* prvectiGravatar filliatr1999-11-26
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-09 14:27:19 +0000