diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-07 07:53:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-07 07:53:42 +0200 |
| commit | 7e8612307f8393f12783bd9c591e6e26a3277b9d (patch) | |
| tree | 669e8e8e973871f693a8d1668273531f30957366 /.mailmap | |
| parent | 876f202985d5bd463bd5b44c195b239bcfedad7c (diff) | |
In Hipattern: some functions not working modulo evar instantiation.
In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
Diffstat (limited to '.mailmap')
0 files changed, 0 insertions, 0 deletions