From 2aa844c9d024e34014b7efb27baa22797b4d079f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 1 Apr 2017 21:05:36 +0200
Subject: [PATCH] Let set_solver/set_unfold only touch Prop hyps.
This is needed to use coq-stdpp in developments with -type-in-type
as set_unfold will otherwise unify with any hyp, causing the
set_solver tactic to break.
---
theories/collections.v | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/theories/collections.v b/theories/collections.v
index 8354bafd..c5d8cc8d 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -270,9 +270,13 @@ End set_unfold_list.
Ltac set_unfold :=
let rec unfold_hyps :=
try match goal with
- | H : _ |- _ =>
- apply set_unfold_1 in H; revert H;
- first [unfold_hyps; intros H | intros H; fail 1]
+ | H : ?P |- _ =>
+ lazymatch type of P with
+ | Prop =>
+ apply set_unfold_1 in H; revert H;
+ first [unfold_hyps; intros H | intros H; fail 1]
+ | _ => fail
+ end
end in
apply set_unfold_2; unfold_hyps; csimpl in *.
--
GitLab