From 2bc4df02f48338acfdf5a16b51f66d9badd82cde Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 1 Jul 2016 23:33:59 +0200 Subject: [PATCH] Use ndot_ne_disjoint more eager so it expands definitions. --- prelude/tactics.v | 9 +++++---- program_logic/namespaces.v | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/prelude/tactics.v b/prelude/tactics.v index 8a471ded5..13e74464c 100644 --- a/prelude/tactics.v +++ b/prelude/tactics.v @@ -412,10 +412,11 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) := It will search for the first subterm of the goal matching [pat], and then call [tac] with that subterm. *) Ltac find_pat pat tac := - match goal with |- context [?x] => - unify pat x with typeclass_instances; - tryif tac x then idtac else fail 2 -end. + match goal with + |- context [?x] => + unify pat x with typeclass_instances; + tryif tac x then idtac else fail 2 + end. (** Coq's [firstorder] tactic fails or loops on rather small goals already. In particular, on those generated by the tactic [unfold_elem_ofs] which is used diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v index a01052b78..ac5d73aba 100644 --- a/program_logic/namespaces.v +++ b/program_logic/namespaces.v @@ -64,7 +64,7 @@ End ndisjoint. (* The hope is that registering these will suffice to solve most goals of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *) Hint Resolve ndisj_subseteq_difference : ndisj. -Hint Extern 0 (_ .@ _ ⊥ _ .@ _) => apply ndot_ne_disjoint; congruence : ndisj. +Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_r : ndisj. -- GitLab