diff options
| author |  blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-04 16:26:51 +0000 |
|---|---|---|
| committer | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-04 16:26:51 +0000 |
| commit | 05f9369c759ecd957585feec6659e3c05e313a11 (patch) | |
| tree | a5754d07e1c74af1dcd1e886bae3988647bc7f98 /common | |
| parent | 7155843b75086379eeaeaa6c89c824aebd58104e (diff) | |
Ajout trunk CompCert
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
| -rw-r--r-- | common/Errors.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/common/Errors.v b/common/Errors.v index a70ea6e..b04d875 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -189,6 +189,8 @@ 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. @@ -200,6 +202,7 @@ 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 _) => |