aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4456.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2015-12-31Fix bug #4456, anomaly in handle-side effectsMatthieu Sozeau
The side-effects can contain universe declarations needed to typecheck later proofs, which weren't added to the env used to typecheck them.