aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Expand)AuthorAge
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...Gravatar herbelin2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Distinction local/globalGravatar herbelin2000-11-27
* Branchement des Local sur des SectionLocalDefGravatar herbelin2000-11-27
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* NettoyageGravatar herbelin2000-11-22
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* code mortGravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* Code mortGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Bug: on tentait de déclarer un schéma d'induction pour un coinductifGravatar herbelin2000-07-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...Gravatar herbelin2000-03-28
* Réparation du cast oublié lors d'une définition castéeGravatar herbelin2000-03-08
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
* Ajout de RecordGravatar herbelin2000-01-11
* message erreur SchemeGravatar herbelin1999-12-15
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Les inductifs dans Scheme doivent être des ident d'inductifsGravatar herbelin1999-12-15
* petite erreur dans CommandGravatar filliatr1999-12-13
* documentation interfacesGravatar filliatr1999-12-13
* modulesGravatar filliatr1999-12-12
* - constantes avec recettesGravatar filliatr1999-12-09
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* premier debugageGravatar filliatr1999-12-05
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module CommandGravatar filliatr1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 22:45:38 +0000