aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.ml
AgeCommit message (Expand)Author
2000-10-01Code mortherbelin
2000-09-14Abstraction de constrherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-01Bug: on tentait de déclarer un schéma d'induction pour un coinductifherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-28Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...herbelin
2000-03-08Réparation du cast oublié lors d'une définition castéeherbelin
2000-01-13Nettoyage des fichiers de parsingherbelin
2000-01-11Ajout de Recordherbelin
1999-12-15message erreur Schemeherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-15Les inductifs dans Scheme doivent être des ident d'inductifsherbelin
1999-12-13petite erreur dans Commandfilliatr
1999-12-13documentation interfacesfilliatr
1999-12-12modulesfilliatr
1999-12-09 - constantes avec recettesfilliatr
1999-12-08deplacement de Discharge dans toplevelfilliatr
1999-12-06declarations eliminations / debuggae inductifs (debut)filliatr
1999-12-05premier debugagefilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-02module Commandfilliatr