aboutsummaryrefslogtreecommitdiff
path: root/toplevel/discharge.ml
AgeCommit message (Expand)Author
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-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-04-21discharge des axiomesfilliatr
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Déplacement des fonctions spécifiques du discharge qui était dans Generic;...herbelin
2000-03-18bug discharge (work_alist contenanti plein de fois les memes choses)filliatr
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
2000-01-11Ajout de Recordherbelin
2000-01-07Déplacement non-affichage des coercions dans termastherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-12modulesfilliatr
1999-12-09 - constantes avec recettesfilliatr
1999-12-09Discharge (encore bugge)filliatr
1999-12-08deplacement de Discharge dans toplevelfilliatr