index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretype_errors.ml
Commit message (
Expand
)
Author
Age
*
pretyping/pretyping.ml
herbelin
2002-09-03
*
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-18
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
GROS COMMIT:
barras
2001-11-05
*
Rustine pour rendre les messages d'erreurs de la compilation des Cases plus l...
herbelin
2001-10-15
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
Ajout erreur GlobalNotFound
herbelin
2000-11-20
*
Messages d'erreurs Cases
herbelin
2000-10-10
*
kernel/type_errors.ml
herbelin
2000-09-06
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Bricoles
herbelin
2000-06-29
*
Afficahge des locations
herbelin
2000-05-31
*
- erreurs Pretype
filliatr
1999-12-10
*
Suppression Rel de rawconstr et correction de bugs d'affichage
herbelin
1999-12-10
*
Ajout des messages d'erreurs de Cases
herbelin
1999-12-09
*
portage modules Evarconv et Evarutil
filliatr
1999-11-29
*
Modification pour faire compiler pretyping.ml qui maintenant compile
herbelin
1999-11-26
*
Versions initiales
herbelin
1999-11-24