From 9e1372f77218ca6f0baf4ed7c590c91ad84b6313 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 25 Jun 2017 16:24:30 +0200
Subject: Moving "assert" (internally "Cut") to the new proof engine.

It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
---
 test-suite/success/forward.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
index 0ed5b524f3..4e36dec15b 100644
--- a/test-suite/success/forward.v
+++ b/test-suite/success/forward.v
@@ -16,3 +16,14 @@ eremember (S (S ?[x])).
 instantiate (x:=0).
 reflexivity.
 Qed.
+
+(* Don't know if it is good or not but the compatibility tells that
+   the asserted goal to prove is subject to beta-iota but not the
+   asserted hypothesis *)
+
+Goal True.
+assert ((fun x => x) False).
+Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *)
+2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *)
+Abort.
+
-- 
cgit v1.2.3


From 4f392bc8114309f388791c1ddc7cc95cc021aa5e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 25 Jun 2017 16:37:55 +0200
Subject: 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).
---
 test-suite/success/ltac.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 1d35f1ef6c..29e373eaa5 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.
-- 
cgit v1.2.3