diff options
| author | Hugo Herbelin | 2015-09-08 12:02:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-08 13:49:55 +0200 |
| commit | f2130a88e1f67d68d1062cce883a7c2666b146d8 (patch) | |
| tree | efdb6140e6fdcc9ebd3fb30c5c823d6c41132a1a /kernel/nativelambda.ml | |
| parent | dea62dfc660ffd61958c50e955f7b962afd83234 (diff) | |
Ensuring that patterns of the form pat/constr move the hypotheses replacing
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions