Adapt to expr.Wf4

Depends on mit-plv/rewriter#124, for https://github.com/JasonGross/fiat-crypto/tree/dont-bottomify
mit-plv · Nov 25, 2023 · 02a09f7 · 02a09f7
1 parent ca174d7
commit 02a09f7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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.