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.mli
Commit message (
Expand
)
Author
Age
*
Repairing r16205: errors raised by check_evar_instance were no longer
herbelin
2013-02-28
*
A more informative message when the elimination predicate for
herbelin
2013-02-17
*
Locating errors from consider_remaining_unif_problems if possible
herbelin
2013-02-17
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Moved code from Pretype_error to Evarutil
ppedrot
2013-02-10
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
A few more betaiota on environments and types of error messages. Seems to
herbelin
2011-03-05
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Quelques bricoles autour de l'unification:
herbelin
2008-04-27
*
Bug squashing day !
msozeau
2008-04-17
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
*
Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...
msozeau
2008-01-18
*
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
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
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
*
Suppression de Rawterm.loc, branchement sur Util.loc
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
*
pretyping/pretyping.ml
herbelin
2002-09-03
*
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-18
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
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
[next]