Changeset 1672 for src/Clight/Csem.ma
 Timestamp:
 Feb 1, 2012, 4:16:06 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r1545 r1672 722 722  eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H) 723 723 ]. 724 724 (* 725 725 inverter eval_expr_inv_ind for eval_expr : Prop. 726 726 *) 727 727 let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem) 728 728 (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop) … … 744 744 ninverter eval_lvalue_inv_ind for eval_lvalue : Prop. 745 745 *) 746 746 (* 747 747 definition eval_lvalue_inv_ind : 748 748 ∀x1: genv. … … 793 793  *: skip 794 794 ] qed. 795 795 *) 796 796 let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem) 797 797 (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
Note: See TracChangeset
for help on using the changeset viewer.