aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-09-04 21:03:55 +0200
committerPierre-Marie Pédrot2014-09-04 21:06:14 +0200
commitba801cd1c9866f39782279e22ceab956c4efd5c6 (patch)
tree99cc8bc1b8ad61de84a03a8eed6110f68f9bca33 /kernel
parent7057e7e9ab1160fc0e176182b6e71f720784715a (diff)
Ensuring the invariant that hypotheses and named context of the environment of
Proofview goals coincide by always using the named context and discarding the hypotheses.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions