From f4d36a60e2e9c0d7ce9d1b318f20e1afb58ae475 Mon Sep 17 00:00:00 2001 From: Christian Doczkal Date: Fri, 11 Dec 2020 16:51:56 +0100 Subject: [PATCH] backward compatible fix for mem_imset renaming --- theories/nfa.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/nfa.v b/theories/nfa.v index 8932f31..a67f001 100644 --- a/theories/nfa.v +++ b/theories/nfa.v @@ -240,7 +240,8 @@ Qed. Lemma enfa_concIr (p : A2) x : nfa_accept p x -> @enfa_accept enfa_conc (inr p) x. Proof. elim: x p => [p Hp|a x IH p /= /exists_inP [q q1 q2]]. - - by constructor; rewrite mem_imset. + - (* compat: //. exact: IH. Qed. @@ -255,7 +256,8 @@ Qed. Lemma enfa_concP x : reflect (enfa_lang enfa_conc x) (conc (nfa_lang A1) (nfa_lang A2) x). Proof. apply: (iffP (@concP _ _ _ _)) => [[x1] [x2] [X1 [X2 X3]] |]. - - case/exists_inP : X2 => s ? ?. exists (inl s); first by rewrite /enfa_conc /= mem_imset. + - (* compat: s ? ?. exists (inl s); first solve [exact: imset_f|exact:mem_imset]. subst. exact: enfa_concIl. - move => [[s /imsetP [? ? [?]] /enfa_concE [x1] [x2] [? ? ?] |s]]; last by case/imsetP. exists x1; exists x2. repeat (split => //). apply/exists_inP. by exists s;subst.