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.
Pierre-Marie Pédrot
2017-07-04
*
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Cleaning up interfaces.
Pierre-Marie Pédrot
2017-02-14
*
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
*
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarsolve API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evardefine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Find_subterm API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
*
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
[next]