From 05f9369c759ecd957585feec6659e3c05e313a11 Mon Sep 17 00:00:00 2001 From: blazy Date: Wed, 4 Jul 2012 16:26:51 +0000 Subject: Ajout trunk CompCert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Errors.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'common') 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 _) => -- cgit v1.2.3