From be9e1f1b6621c065f13a20b393440c5764589c23 Mon Sep 17 00:00:00 2001 From: project_18556810_bot Date: Mon, 6 Jan 2025 12:54:06 +0000 Subject: [PATCH] [github pages] BRiCk documentation created from 43759fa8 --- .../coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.expr.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.expr.html b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.expr.html index cbc95bf2..d8829861 100644 --- a/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.expr.html +++ b/docs/_static/coqdoc/bedrock.lang.html/bedrock.lang.cpp.logic.expr.html @@ -692,7 +692,7 @@

bedrock.lang.cpp.logic.expr

        (letI* '(la, rv), free :=
           eval2 (evaluation_order.order_of OOEqual) (wp_lval l) (wp_operand r) in
            la |-> anyR (erase_qualifiers ty) (cQp.mut 1) **
-           (la |-> primR (erase_qualifiers ty) (cQp.mut 1) rv -* Q la free))
+           (la |-> tptstoR (erase_qualifiers ty) (cQp.mut 1) rv -* Q la free))
        |-- wp_lval (Eassign l r ty) Q.