aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.ml
Commit message (Expand)AuthorAge
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Ajout implicits_of_global + accès par noms longsGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* L'état implicite des définitions survivant au discharge redevient celui du ...Gravatar herbelin2000-10-23
* Renommage canonique :Gravatar herbelin2000-10-18
* Prise en compte de l'environnement dans le calcul des implicitesGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* suppression de Fw pour les implicitesGravatar herbelin2000-05-03
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* modulesGravatar filliatr1999-12-12
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* poursuite de VernacentriesGravatar filliatr1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* module TermastGravatar filliatr1999-11-26
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* juste l'interface de DischargeGravatar filliatr1999-09-28
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 18:22:19 +0000