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
*
Bump year in headers.
Maxime Dénès
2017-06-01
*
Reserve exception "ConversionFailed" in unification for failure of
Hugo Herbelin
2016-06-12
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
Added a CannotSolveConstraint unification error and made experiments
Hugo Herbelin
2014-12-11
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Fixing #3634 (wrong env in "cannot instantiate because not in its
Hugo Herbelin
2014-10-03
*
Move UnsatisfiableConstraints to a pretype error.
Matthieu Sozeau
2014-08-22
*
Moved code for finding subterms (pattern, induction, set, generalize, ...)
Hugo Herbelin
2014-06-28
*
Made the subterm finding function make_abstraction independent of the
Hugo Herbelin
2014-06-28
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Merging Context and Sign.
ppedrot
2013-04-29
*
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
[next]