diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-11 17:51:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
| commit | dd243f5f35200aa9fdcc400300990192ed4bc0b6 (patch) | |
| tree | 8f3558aaefae2e789610cfb6c1c61e281b50f3f8 | |
| parent | b4130798bd428ad3586baa17b0f991018854997a (diff) | |
| download | compcert-dd243f5f35200aa9fdcc400300990192ed4bc0b6.tar.gz compcert-dd243f5f35200aa9fdcc400300990192ed4bc0b6.zip | |
Errors: fixed a loop in tactic MonadInv
| -rw-r--r-- | common/Errors.v | 2 |
1 files changed, 1 insertions, 1 deletions
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) => |