From dd243f5f35200aa9fdcc400300990192ed4bc0b6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 11 Jun 2019 17:51:12 +0200 Subject: Errors: fixed a loop in tactic MonadInv --- common/Errors.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common') diff --git a/common/Errors.v b/common/Errors.v index 28933313..6807735a 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -164,7 +164,7 @@ Ltac monadInv1 H := | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) => destruct X; [try (monadInv1 H) | discriminate] | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) => - destruct X as [] eqn:?; [discriminate | try (monadInv1 H)] + destruct X as [] eqn:?; simpl negb in H; [discriminate | try (monadInv1 H)] | (match ?X with true => _ | false => assertion_failed end = OK _) => destruct X as [] eqn:?; [try (monadInv1 H) | discriminate] | (mmap ?F ?L = OK ?M) => -- cgit