Revert "Documentation about the introduction of attributes in the API"

This reverts commit 1f45ff36.

examples/use_api/mlw_expr.ml

@@ -28,7 +28,7 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
 
 declaration of
 BEGIN{source2}
-     let f2 [@foo] () : int
+     let f2 () : int
         requires { true }
         ensures { result >= 0 }
       = let x = ref 42 in !x
@@ -63,8 +63,7 @@ let get_fun : Expr.rsymbol =
 
 (* BEGIN{code2} *)
 let d2 =
-  let attrs = Ident.(Sattr.singleton (create_attribute "foo")) in
-  let id = Ident.id_fresh ~attrs "f" in
+  let id = Ident.id_fresh "f" in
   let post =
     let result =
       Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int

examples/use_api/mlw_tree.ml

@@ -96,7 +96,7 @@ let mod_M1 =
 (* declaration of
   BEGIN{source2}
 module M2
-  let f [@foo] (x:int) : int
+  let f (x:int) : int
     requires { x=6 }
     ensures { result=42 }
    = x*7
@@ -137,9 +137,7 @@ let mod_M2 =
       Efun(param1 id_x int_type, None, mk_pat Pwild,
            Ity.MaskVisible, spec, body)
     in
-    let attr = ATstr (Ident.create_attribute "foo") in
-    let id = { (mk_ident "f") with id_ats = [attr] } in
-    Dlet(id,false,Expr.RKnone, mk_expr f)
+    Dlet(mk_ident "f",false,Expr.RKnone, mk_expr f)
   in
   (mk_ident "M2",[use_int_Int ; f])
 (* END{code2} *)