index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
/
loc.ml
Commit message (
Expand
)
Author
Age
*
[api] Remove 8.7 ML-deprecated functions.
Emilio Jesus Gallego Arias
2017-11-07
*
Reporting locations in error messages about notation formats.
Hugo Herbelin
2017-09-18
*
Using an algebraic type for distinguishing toplevel input from location in file.
Hugo Herbelin
2017-09-14
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[location] Cleanup.
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Remove `Loc.internal_ghost`
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
*
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
*
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
*
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-20
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Do not dump a glob reference when its location is ghost. (Fix bug #4469)
Guillaume Melquiond
2015-12-31
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
More equality functions
ppedrot
2012-11-25
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
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