diff options
Diffstat (limited to 'common/Errors.v')
-rw-r--r-- | common/Errors.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/common/Errors.v b/common/Errors.v index b04d875d..a70ea6ea 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -189,8 +189,6 @@ Ltac monadInv1 H := | (assertion ?b = OK ?X) => let A := fresh "A" in (generalize (assertion_inversion _ H); intro A); clear H - | (let _ := _ in ?Y) => - monadInv1 Y | (mmap ?F ?L = OK ?M) => generalize (mmap_inversion F L H); intro end. @@ -202,7 +200,6 @@ Ltac monadInv H := | (bind ?F ?G = OK ?X) => monadInv1 H | (bind2 ?F ?G = OK ?X) => monadInv1 H | (assertion _ = OK _) => monadInv1 H - | (let _ := ?X in OK _ = OK _) => destruct X as [[XT XM] XV]; monadInv1 H | (?F _ _ _ _ _ _ _ _ = OK _) => ((progress simpl in H) || unfold F in H); monadInv1 H | (?F _ _ _ _ _ _ _ = OK _) => |