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
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
Documentation
herbelin
2006-01-29
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
Nouvelle en-tête
herbelin
2004-07-16
*
Suppression de Rawterm.loc, branchement sur Util.loc
herbelin
2004-07-16
*
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