Update docs: EasyCrypt/easycrypt@8218a6f

Author: github-actions[bot]

refman/_sources/tactics/skip.rst.txt

@@ -16,7 +16,7 @@ The ``skip`` tactic does not attempt to solve this logical obligation itself.
    :local:
 
 ------------------------------------------------------------------------
-Variant: ``skip`` (Hoare logic)
+Variant: ``skip`` (HL)
 ------------------------------------------------------------------------
 
 .. ecproof::
@@ -39,15 +39,15 @@ Variant: ``skip`` (Hoare logic)
    abort.
 
 ------------------------------------------------------------------------
-Variant: ``skip`` (Relational Probabilistic Hoare logic)
+Variant: ``skip`` (pRHL)
 ------------------------------------------------------------------------
 
 In the relational Hoare logic setting, the `skip`` tactic applies only
 when both programs are empty, in which case it reduces the relational
 judgment to obligations on the preconditions and postconditions alone.
 
 .. ecproof::
-   :title: Relational Hoare logic example
+   :title: Probabilistic Relational Hoare logic example
 
    require import AllCore.
 
@@ -66,7 +66,7 @@ judgment to obligations on the preconditions and postconditions alone.
    abort.
 
 ------------------------------------------------------------------------
-Variant: ``skip`` (Probabilistic Hoare logic)
+Variant: ``skip`` (pHL)
 ------------------------------------------------------------------------
 
 In the probabilistic Hoare logic setting, applying ``skip`` generates an
@@ -93,3 +93,31 @@ must also prove that the probability weight of the empty program, namely
    proof.
      proc. (*$*) skip.
    abort.
+
+------------------------------------------------------------------------
+Variant: ``skip`` (eHL)
+------------------------------------------------------------------------
+
+In expectation Hoare logic, where the precondition and postcondition are
+respectively a pre-expectation and a post-expectation, applying skip generates
+the obligation to prove that the post-expectation is bounded above by the
+pre-expectation.
+
+.. ecproof::
+   :title: Expectation Hoare logic example
+
+   require import AllCore Xreal.
+   
+   module M = {
+     proc f(x : int) = {
+       return x;
+     }
+   }.
+   
+   op p : int -> xreal.
+   op q : int -> xreal.
+   
+   lemma L : ehoare[M.f : p x ==> q res].
+   proof.
+     proc. (*$*) skip.
+   abort.

refman/_static/proofnav/proofnav.bundle.js

@@ -17,7 +17,7 @@
       <script src="_static/documentation_options.js?v=5929fcd5"></script>
       <script src="_static/doctools.js?v=9bcbadda"></script>
       <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
-      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=5e5ff161"></script>
+      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=3ab35e3c"></script>
       <script src="_static/design-tabs.js?v=f930bc37"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="#" />

refman/_static/proofnav/proofnav.bundle.js.map

@@ -18,7 +18,7 @@
       <script src="_static/documentation_options.js?v=5929fcd5"></script>
       <script src="_static/doctools.js?v=9bcbadda"></script>
       <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
-      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=5e5ff161"></script>
+      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=3ab35e3c"></script>
       <script src="_static/design-tabs.js?v=f930bc37"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />

refman/genindex.html

@@ -18,7 +18,7 @@
       <script src="_static/documentation_options.js?v=5929fcd5"></script>
       <script src="_static/doctools.js?v=9bcbadda"></script>
       <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
-      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=5e5ff161"></script>
+      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=3ab35e3c"></script>
       <script src="_static/design-tabs.js?v=f930bc37"></script>
     <script src="_static/js/theme.js"></script>
     <script src="_static/searchtools.js"></script>

refman/index.html

@@ -18,7 +18,7 @@
       <script src="_static/documentation_options.js?v=5929fcd5"></script>
       <script src="_static/doctools.js?v=9bcbadda"></script>
       <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
-      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=5e5ff161"></script>
+      <script defer="defer" src="_static/proofnav/proofnav.bundle.js?v=3ab35e3c"></script>
       <script src="_static/design-tabs.js?v=f930bc37"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />