aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2000-05-22Bugs d'index d'inductiveherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-18Adaptation pour nouveaux inductifs (cf Inductive)herbelin
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
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-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Nettoyageherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
2000-01-20Broutillesherbelin
2000-01-07Correction pbs liés aux evarherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-14sauvegarde de la valeur de module_namefilliatr
1999-12-13mise a jour de refiner.ml (reports de modifs de la V6.3)barras
1999-12-13 - méthode load sur les Hintsfilliatr
1999-12-12modulesfilliatr
1999-12-10bug: enregistrement de vartab au lieu de csttabfilliatr
1999-12-10 - erreurs Pretypefilliatr
1999-12-10debug resetfilliatr
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-03module Discharge (ne fait rien pour l'instant)filliatr
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-02Pfedit (fin)filliatr
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
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-27fin Recordops, et debut Evarutilfilliatr
1999-11-26Déplacement fonction transform_rec vers pretypingherbelin
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
1999-11-26prvectifilliatr
1999-11-26module Termastfilliatr
1999-11-26module Goptions (etait Options)filliatr
1999-11-26Evd vient apres Environ -> id_of_existential expansefilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:20:31 +0000