aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
Commit message (Expand)AuthorAge
* Prise en compte des définitions localesGravatar herbelin2000-11-27
* sp au lieu de id dans END-SECTIONGravatar herbelin2000-11-26
* 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
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Petit bug entre close_section'sGravatar herbelin2000-11-20
* Tables séparées pour chaque type de global; calcul de la Nametab de la sect...Gravatar herbelin2000-11-20
* 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
* Rétablissement compatibilité des implicites (2ème) (mais amélioration)Gravatar herbelin2000-10-23
* L'état implicite des définitions survivant au discharge redevient celui du ...Gravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Hypotheses des ind oubliees dans le dischargeGravatar herbelin2000-10-12
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* 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
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* discharge des axiomesGravatar filliatr2000-04-21
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Déplacement des fonctions spécifiques du discharge qui était dans Generic;...Gravatar herbelin2000-03-21
* bug discharge (work_alist contenanti plein de fois les memes choses)Gravatar filliatr2000-03-18
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Ajout de RecordGravatar herbelin2000-01-11
* Déplacement non-affichage des coercions dans termastGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* modulesGravatar filliatr1999-12-12
* - constantes avec recettesGravatar filliatr1999-12-09
* Discharge (encore bugge)Gravatar filliatr1999-12-09
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 12:27:59 +0000