diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-06 07:20:25 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-06 07:20:25 +0000 |
| commit | c72b9a5bf321bfc05419eae50a5a27be03739bda (patch) | |
| tree | 52a288695f218236425c1f03026524296116cd8a /common | |
| parent | 1d4ca9226236135526d095a8c575571a297cfcb7 (diff) | |
Revert unintentional commit #1955
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
| -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 b04d875..a70ea6e 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 _) => |