From 8c00ea66abf1f2fd702c45771ff32192c7f93271 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 25 Nov 2023 14:03:15 -0800
Subject: [PATCH] Adapt to expr.Wf4

Depends on https://github.com/mit-plv/rewriter/pull/124, for
https://github.com/JasonGross/fiat-crypto/tree/dont-bottomify
---
 README.md              | 2 +-
 src/Language/WfExtra.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index bb8bf8c4e7..a3b30295c5 100644
--- a/README.md
+++ b/README.md
@@ -640,7 +640,7 @@ For `Language.v`, there is a semi-arbitrary split between two files
 
 - `Wf.v`: Depends on `Inversion.v`
   Defines:
-  + expr.wf, expr.Wf, expr.wf3, expr.Wf3
+  + expr.wf, expr.Wf, expr.wf3, expr.wf4, expr.Wf3, expr.Wf4
   + GeneralizeVar.Flat.wf
   + `expr.inversion_wf` (and variants), which invert `wf` hypotheses
   + `expr.wf_t` (and variants wf_unsafe_t and wf_safe_t) which make
diff --git a/src/Language/WfExtra.v b/src/Language/WfExtra.v
index 438f438468..e958438036 100644
--- a/src/Language/WfExtra.v
+++ b/src/Language/WfExtra.v
@@ -17,7 +17,7 @@ Module Compilers.
 #[global]
   Hint Opaque expr.interp expr.Interp : interp_extra.
 #[global]
-  Hint Opaque expr.Wf expr.Wf3 : wf_extra interp_extra.
+  Hint Opaque expr.Wf expr.Wf3 expr.Wf4 : wf_extra interp_extra.
 
   Module expr.
     Import Language.Wf.Compilers.expr.
@@ -26,8 +26,8 @@ Module Compilers.
     Global Hint Opaque expr.APP : wf_extra interp_extra.
 #[global]
     Hint Rewrite @expr.Interp_APP : interp_extra.
-    Global Hint Immediate Wf_of_Wf3 : wf_extra.
-    Global Hint Resolve Wf3_of_Wf : wf_extra.
+    Global Hint Immediate Wf_of_Wf3 Wf_of_Wf4 : wf_extra.
+    Global Hint Resolve Wf3_of_Wf Wf4_of_Wf : wf_extra.
 
     Definition Wf_base_Reify_as {t} v
       := @Wf_base_Reify_as base.type.base base.base_interp base.type.base_beq ident ident.buildIdent base.reflect_base_beq t v.