aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2000-11-03compilation avec make de Solaris; README et INSTALLfilliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-30Ajout d'un switch pour le debuggerdelahaye
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
2000-10-24Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageherbelin
2000-10-23Rétablissement compatibilité des implicites (2ème) (mais amélioration)herbelin
2000-10-23Import de Infix au Requireherbelin
2000-10-23code mortherbelin
2000-10-23L'état implicite des définitions survivant au discharge redevient celui du ...herbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-16Correction bug affichage des infixherbelin
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...herbelin
2000-10-12Hypotheses des ind oubliees dans le dischargeherbelin
2000-10-11Message d'erreur bad patternherbelin
2000-10-10Messages d'erreurs Casesherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01renommage map_constr_with_named_bindersherbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
2000-10-01Code mortherbelin
2000-09-15Messages d'erreursherbelin
2000-09-15Expression anglaiseherbelin
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-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...herbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-09-06kernel/type_errors.mlherbelin
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-21retablissement minicoq (pour Jacek)filliatr
2000-07-21Fail n + appel de interpdelahaye
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-07-01Bug: on tentait de déclarer un schéma d'induction pour un coinductifherbelin
2000-06-29Essai de simplification compte tenu de l'info de locationherbelin
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-02Bugs/Messages d'erreursherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-25Petit bug get_current_contextherbelin
2000-05-22Renommage hypothèses de nom redondant dans les environnementsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18export get_current_contextherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-27 11:22:15 +0000