aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* nouveau load pathGravatar filliatr2000-11-08
* améliorationGravatar herbelin2000-11-08
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* print_idl inlinéGravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* compilation avec make de Solaris; README et INSTALLGravatar filliatr2000-11-03
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Ajout d'un switch pour le debuggerGravatar delahaye2000-10-30
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
* Meilleur endroit pour déclarer les parseurs de grammaires et joli affichageGravatar herbelin2000-10-24
* Rétablissement compatibilité des implicites (2ème) (mais amélioration)Gravatar herbelin2000-10-23
* Import de Infix au RequireGravatar herbelin2000-10-23
* code mortGravatar herbelin2000-10-23
* L'état implicite des définitions survivant au discharge redevient celui du ...Gravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Correction bug affichage des infixGravatar herbelin2000-10-16
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Hypotheses des ind oubliees dans le dischargeGravatar herbelin2000-10-12
* Message d'erreur bad patternGravatar herbelin2000-10-11
* Messages d'erreurs CasesGravatar herbelin2000-10-10
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* renommage map_constr_with_named_bindersGravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Code mortGravatar herbelin2000-10-01
* Messages d'erreursGravatar herbelin2000-09-15
* Expression anglaiseGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Fail n + appel de interpGravatar delahaye2000-07-21
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Bug: on tentait de déclarer un schéma d'induction pour un coinductifGravatar herbelin2000-07-01
* Essai de simplification compte tenu de l'info de locationGravatar herbelin2000-06-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 04:11:42 +0000