aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/PLACEHOLDER.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-10-21 10:49:15 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-10-21 12:24:43 +0200
commit5b0b6c92354c34a4f0d5551f88b16264fb08be5f (patch)
treeb789f64d3024e70a70a1c175facab638dde76367 /test-suite/bugs/closed/PLACEHOLDER.v
parenta5b977e3acb6d2cd73ed6c895a7d4b587366caa9 (diff)
This makes [refine] typecheck the term only once (instead of twice), (Qed excluded of course). Fix test-suite file for output of constraints accordingly.
Diffstat (limited to 'test-suite/bugs/closed/PLACEHOLDER.v')
0 files changed, 0 insertions, 0 deletions