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
*
Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...
msozeau
2008-01-18
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Suppression des type_app et body_of_type qui alourdissent inutilement le code
herbelin
2007-08-27
*
Utilisation de l'environnement pour l'affichage de certains messages d'erreurs
herbelin
2007-02-21
*
Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...
notin
2006-10-05
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
Changement des named_context
gregoire
2005-12-02
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
bug #790: better error_not_clean
barras
2004-07-13
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Localisation
herbelin
2003-01-19
*
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