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
*
Moving potentially costly computation from exception raising to message
ppedrot
2013-10-22
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Repairing r16205: errors raised by check_evar_instance were no longer
herbelin
2013-02-28
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Displaying environment and unfolding aliases in "cannot_unify"
herbelin
2013-02-17
*
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
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
A bit of documentation around cases.ml + ML modules uselessly open
herbelin
2011-11-16
*
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
*
Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"
herbelin
2010-06-13
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Removing some betaiota-redexes in error messages (an experiment)
herbelin
2010-01-12
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
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
*
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
[next]