aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-08-20 12:58:27 +0200
committerGaëtan Gilbert2019-08-23 23:12:05 +0200
commitb3e4a58e21c042c8610b2f81ccafd4a2c3f74b3a (patch)
tree1b9ce522dc475c486991752bd9f7adc38acefae3 /kernel
parentadcbcbe743e0508a1fc3cd3eb18f73b00db1d55e (diff)
coqchk: Cleanup environment manipulation in check_constant_declaration
Instead of doing (simplified code) ~~~ocaml let check env kn cb = let flags = env.flags in let env' = set_flags env cb.flags in ... let env = add_constant cb kn (if poly then env else env') in set_flags env flags ~~~ (NB: when not poly env' has only the typing flags different from env) we do ~~~ocaml let check env kn cb = let env = set_flags env cb.flags in ... () let check env kn cb = let () = check env kn cb in add_constant cb kn env ~~~
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions