aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Arith_base.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-26 16:37:26 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-27 00:28:50 +0200
commit05bd0ab1dd85764874ca077005dcaff5414589a5 (patch)
tree40ecae5fc60a644761898bcb61e13ef463efecb6 /theories/Arith/Arith_base.v
parentb818c00e3e895ea9b736ab968e3ba109b0fd67c1 (diff)
Moving setting of "cleared" evar flag directly in Evd.restrict.
In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further.
Diffstat (limited to 'theories/Arith/Arith_base.v')
0 files changed, 0 insertions, 0 deletions