aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Expand)AuthorAge
* GROS COMMIT:Gravatar barras2001-11-05
* Vérification précoce qu'un lemme n'existe pas déjàGravatar herbelin2001-10-26
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...Gravatar herbelin2001-09-19
* Transformation de Remark/Fact en constantes non visibles sans qualificationGravatar herbelin2001-09-14
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* ParsingGravatar herbelin2001-08-10
* anomaly -> errorGravatar clrenard2001-07-10
* Changement de la structure des points fixesGravatar barras2001-05-03
* un typage sûr pour Goal et CheckGravatar filliatr2001-04-20
* Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par GoalGravatar herbelin2001-04-09
* Uniformisation des 'Save def_tok id'Gravatar herbelin2001-04-09
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
* entetesGravatar filliatr2001-03-15
* Erreur sur commitGravatar herbelin2001-02-14
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 12:18:15 +0000