index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
coercion.mli
Commit message (
Expand
)
Author
Age
*
Mise en place de coercion dans les motifs
herbelin
2001-12-11
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
L'instantiation des evars quand un produit ou une sorte étaient attendus n'Ã...
herbelin
2001-09-14
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Insertion de coercion au milieu des applications partielles et propagation de...
herbelin
2000-11-08
*
Nettoyage Coercion
herbelin
2000-10-19
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Séparation des contraintes de type et de valeur dans pretyping
herbelin
2000-06-29
*
Bugs et simplifications coercions
herbelin
2000-06-02
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Afficahge des locations
herbelin
2000-05-31
*
Export inh_conv_coerce_to et divers
herbelin
2000-03-07
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
mise a jour Coercion
filliatr
1999-12-01
*
- environment -> safe_environment
filliatr
1999-12-01
*
ocamlweb
filliatr
1999-11-30
*
Modification pour faire compiler pretyping.ml qui maintenant compile
herbelin
1999-11-26
*
Versions initiales
herbelin
1999-11-24