aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
Commit message (Expand)AuthorAge
* Suppression StronglyClassical, StronglyConstructive devient plus concretement...Gravatar herbelin2003-11-08
* Set devient predicatif par defautGravatar herbelin2003-10-28
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
* Déplacement du hash-consing vers declare.mlGravatar herbelin2002-12-10
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Activation du hash-consingGravatar herbelin2002-09-29
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
* suppression de pop_namedGravatar barras2002-02-22
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* Oubli des contraintes d'univers lors de la suppression des cast dans un commi...Gravatar herbelin2001-11-21
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Suppression des Cast externes dans les définitionsGravatar herbelin2001-11-20
* Mise en place d'une méthode directe pour indiquer le type des déclarations ...Gravatar herbelin2001-11-19
* GROS COMMIT:Gravatar barras2001-11-05
* 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
* repare la perte d'opacite a la fermeture de sectionGravatar barras2001-09-21
* TransparentGravatar barras2001-09-20
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* un typage sûr pour Goal et CheckGravatar filliatr2001-04-20
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* réparation (?) discharge axiomeGravatar filliatr2001-03-06
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Changement de subst_metaGravatar mohring2001-02-28
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
* Petite réorganisationGravatar herbelin2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Prise en compte de la contrainte de type dans Definition comme étant un cast...Gravatar herbelin2000-11-29
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* Bug dans le calcul des dépendances dans add_discharged_constantGravatar herbelin2000-11-27
* Reparation bug mutuels indGravatar mohring2000-11-22
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01