Changeset 2500 for src/common/Errors.ma

Timestamp:

Nov 28, 2012, 5:57:38 PM (7 years ago)

Author:

garnier

Message:

Continuing work on simulation in Clight/Cminor?

File:

• src/common/Errors.ma (modified) (1 diff)

src/common/Errors.ma

@@ -273 +273 @@
   ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
   bind2_eq ??? f g = return z →
-  ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧ g x y Eq = return z.
+  ∃x. ∃y. ∃Eq. g x y Eq = return z.
 #A #B #C #f cases f
-[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ??)} @conj try @refl @Heq
+[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? (OK ? 〈a,b〉))} @Heq
 | #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
-qed. 
+qed.
 
 definition res_to_opt : ∀A:Type[0]. res A → option A ≝