index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
/
loc.ml
Age
Commit message (
Expand
)
Author
2021-04-23
Locations: Moving functions Ploc.sub and Ploc.after to loc.ml.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-03-29
[parser] initialization based on Loc.t rather than Loc.source
Enrico Tassi
2019-02-05
Remove the comment fields of locations.
Pierre-Marie Pédrot
2018-11-30
[gramlib] Remove `Ploc.t` in favor of `Loc.t`
Emilio Jesus Gallego Arias
2018-04-04
Fixing #7100 (lost of main file location in case of Ltac failure in other file).
Hugo Herbelin
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-07
[api] Remove 8.7 ML-deprecated functions.
Emilio Jesus Gallego Arias
2017-09-18
Reporting locations in error messages about notation formats.
Hugo Herbelin
2017-09-14
Using an algebraic type for distinguishing toplevel input from location in file.
Hugo Herbelin
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-04-25
[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-24
[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
2016-08-19
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-06-20
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-01-20
Update copyright headers.
Maxime Dénès
2015-12-31
Do not dump a glob reference when its location is ghost. (Fix bug #4469)
Guillaume Melquiond
2015-01-12
Update headers.
Maxime Dénès
2014-12-16
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2013-02-18
Removing Exc_located and using the new exception enrichement
ppedrot
2012-11-25
More equality functions
ppedrot
2012-10-04
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-08-08
Updating headers.
herbelin
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
