Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r726 r797  
    2626[ #a #k #IH #v' #p #H whd in H ⊢ %; elim H; #r #H' %{ r} @IH @H'
    2727| #v #v' #p #H @H
    28 | #a #b *;
     28| #a #b #c *;
    2929] qed.
    3030
    3131lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
    32 #A #a #v' cases a; //; whd in ⊢ (% → ?); *;
     32#A #a #v' cases a; // #m whd in ⊢ (% → ?) *;
    3333qed.
    3434
     
    3636#A #P #e #v cases e;
    3737[ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
    38 | *;
     38| #m *;
    3939] qed.
    4040
     
    7777  ]
    7878| destruct (e3) skip (e13); //
    79 ] qed.
    80 
    81 lemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    82 yields A a v' →
    83 yields_sig A P (err_inject A P (Some ? a) p) v'.
    84 #A #P #a cases a;
    85 [ #v #v' #p #H @H
    86 | #a #b *;
    8779] qed.
    8880
Note: See TracChangeset for help on using the changeset viewer.