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
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
|
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
Evar-normalizing functions now act on EConstrs.
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
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
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
*
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
[next]