diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-25 16:37:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-25 21:30:09 +0200 |
| commit | 4f392bc8114309f388791c1ddc7cc95cc021aa5e (patch) | |
| tree | 5d002b17dbecea4ccee77afeb26debc2458a9021 /test-suite/success/ltac.v | |
| parent | 9e1372f77218ca6f0baf4ed7c590c91ad84b6313 (diff) | |
Reorganizing functions to find the relative position of an hypothesis.
Also fixing a bug of get_next_hyp_position when the hypothesis is the
oldest of the context (see test in ltac.v).
Diffstat (limited to 'test-suite/success/ltac.v')
| -rw-r--r-- | test-suite/success/ltac.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 1d35f1ef6..29e373eaa 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -337,3 +337,14 @@ Goal True. evar (0=0). Abort. +(* Test location of hypothesis in "symmetry in H". This was broken in + 8.6 where H, when the oldest hyp, was moved at the place of most + recent hypothesis *) + +Goal 0=1 -> True -> True. +intros H H0. +symmetry in H. +(* H should be the first hypothesis *) +match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *) +exact (eq_refl H0). +Abort. |