index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
explainErr.ml
Age
Commit message (
Expand
)
Author
2019-07-07
[error] Remove special error printing pre-processing
Emilio Jesus Gallego Arias
2019-07-02
[declare] Cleanup on imports, move exception.
Emilio Jesus Gallego Arias
2019-06-18
[errors] remove "is_handled" logic, turn unhandled into anomalies
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-11
Fix #10225 (Instance := {} accepts duplicate fields)
Gaëtan Gilbert
2019-02-25
Fix #9631: Instance: anomaly grounding non evar-free term
Gaëtan Gilbert
2019-02-11
Fix #9527: unknown evar in nonterminating [fix] error.
Gaëtan Gilbert
2019-02-05
Remove the Plexing.Error exception.
Pierre-Marie Pédrot
2019-01-21
Move inductive_error to Type_errors
Gaëtan Gilbert
2018-11-28
Factor out common code in numeral/string notations
Jason Gross
2018-11-28
Add `String Notation` vernacular like `Numeral Notation`
Jason Gross
2018-11-21
[gramlib] [build] Switch make-based system to packed gramlib
Emilio Jesus Gallego Arias
2018-11-04
Remove the deprecated Token module and port the corresponding code.
Pierre-Marie Pédrot
2018-09-28
Functionalizing calls to the environment in Himsg.
Hugo Herbelin
2018-09-19
Fix Numeral Notations (2/4 - exceptions, usr_err)
Jason Gross
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-17
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-09
[nativecomp] Remove ad-hoc handling of Dynlink exception.
Emilio Jesus Gallego Arias
2017-12-11
[proof] Embed evar_map in RefinerError exception.
Emilio Jesus Gallego Arias
2017-11-21
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
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-11
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-07
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-21
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Prepare for serialization, remove opaque glue.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`
Emilio Jesus Gallego Arias
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias
