index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
safe_typing.ml
Commit message (
Expand
)
Author
Age
*
suppression de pop_named
barras
2002-02-22
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
Oubli des contraintes d'univers lors de la suppression des cast dans un commi...
herbelin
2001-11-21
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
Suppression des Cast externes dans les définitions
herbelin
2001-11-20
*
Mise en place d'une méthode directe pour indiquer le type des déclarations ...
herbelin
2001-11-19
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
repare la perte d'opacite a la fermeture de section
barras
2001-09-21
*
Transparent
barras
2001-09-20
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Mécanisme pour faire remonter les contraintes de typage sur les variables de...
herbelin
2001-09-09
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Changement de la structure des points fixes
barras
2001-05-03
*
un typage sûr pour Goal et Check
filliatr
2001-04-20
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
réparation (?) discharge axiome
filliatr
2001-03-06
*
nouvelle implantation de la reduction
barras
2001-03-01
*
Changement de subst_meta
mohring
2001-02-28
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
- suppression mind_extract_params
filliatr
2000-12-15
*
Petite réorganisation
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Prise en compte de la contrainte de type dans Definition comme étant un cast...
herbelin
2000-11-29
*
Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage
herbelin
2000-11-29
*
Bug dans le calcul des dépendances dans add_discharged_constant
herbelin
2000-11-27
*
Reparation bug mutuels ind
mohring
2000-11-22
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
- simplification Makefile (compilation des fichiers .ml'; pas encore parfait
filliatr
2000-10-31
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
correction bug univers (dummy_univ)
filliatr
2000-10-06
*
Renommage AppL en App
herbelin
2000-10-01
*
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-12
*
Correction pour make doc
herbelin
2000-09-10
*
Suppression de Abst
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
herbelin
2000-09-06
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
retablissement minicoq (pour Jacek)
filliatr
2000-07-21
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Broutilles
herbelin
2000-06-29
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs
herbelin
2000-05-31
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Commentaires
herbelin
2000-04-26
[next]