Update examples

Author: lyonel2017

examples/exception.ec

@@ -1,19 +1,19 @@
 require import AllCore.
 
-exception toto.
-exception tata.
+exception e1.
+exception e2.
 
 module M ={
   proc truc (x:int) : int = {
     if (x = 3)  {
-       raise toto;
+       raise e1;
     } else { x <- 5; }
   return x;
   }
 }.
 
 lemma truc (_x: int):
-hoare [M.truc : _x = x ==> (4 < res) | toto:(_x = 3) | tata:(false) ].
+hoare [M.truc : _x = x ==> (4 < res) | e1:_x = 3 | e2:false ].
     proof.
       proc.
        conseq (: _ ==> x = 5).
@@ -78,7 +78,6 @@ hoare [M'.truc : p8 ==> q3 | assume:q1 |assert: q2 ].
 admitted.
 
 
-(*Conseq is brocken, should take into account the post of exception*)
   lemma assert_assume' :
 hoare [M'.truc : p9 ==> p4 | assume:p6 |assert: p5 ].
     proof.