From eac00ee5b64f07e786c4027ceae360b8faac2600 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Oct 2020 19:42:10 +0200
Subject: [PATCH] Make `solve_inG` faster.
1.) First `simpl` away all the functors 2.) Don't use `done`, which calls `split`.
---
theories/base_logic/lib/own.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 0c4979082..fb6601ad1 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -45,12 +45,12 @@ Ltac solve_inG :=
repeat match goal with
| H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
end;
- (* Again get all assumptions *)
- intros;
+ (* Again get all assumptions and simplify the functors *)
+ intros; simpl in *;
(* We support two kinds of goals: Things convertible to inG;
and records with inG and typeclass fields. Try to solve the
first case. *)
- try done;
+ try assumption;
(* That didn't work, now we're in for the second case. *)
split; (assumption || by apply _).
--
GitLab