aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4782.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2016-06-27More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Hugo Herbelin
2016-06-12Another fix to #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin
2016-06-11Fixing #4782 (a typing error not captured when dealing with bindings).Hugo Herbelin