index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
impargs.ml
Commit message (
Expand
)
Author
Age
*
entetes
filliatr
2001-03-15
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
implicites manuels
filliatr
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Ajout implicits_of_global + accès par noms longs
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
L'état implicite des définitions survivant au discharge redevient celui du ...
herbelin
2000-10-23
*
Renommage canonique :
herbelin
2000-10-18
*
Prise en compte de l'environnement dans le calcul des implicites
herbelin
2000-10-11
*
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
*
correction bug univers (dummy_univ)
filliatr
2000-10-06
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Précalcul de la forme canonique des constructeurs et arités pour traiter le...
herbelin
2000-07-01
*
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
*
suppression de Fw pour les implicites
herbelin
2000-05-03
*
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
herbelin
2000-04-20
*
modules
filliatr
1999-12-12
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
Intégration du Termast et du Retyping de HH, et modifications connexes
herbelin
1999-12-01
*
poursuite de Vernacentries
filliatr
1999-12-01
*
- environment -> safe_environment
filliatr
1999-12-01
*
- Typing -> Safe_typing
filliatr
1999-12-01
*
module Termast
filliatr
1999-11-26
*
- déplacement (encore une fois !) des variables existentielles : elles sont
filliatr
1999-10-18
*
juste l'interface de Discharge
filliatr
1999-09-28
*
- un effort sur la doc (ocamlweb)
filliatr
1999-09-19