diff options
| author | Arnaud Spiwack | 2014-08-07 07:53:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-07 07:53:42 +0200 |
| commit | 7e8612307f8393f12783bd9c591e6e26a3277b9d (patch) | |
| tree | 669e8e8e973871f693a8d1668273531f30957366 /kernel/nativelambda.ml | |
| 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 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions