Bump rewriter to split off Reify file (#1349)

mit-plv · Nov 13, 2022 · 420c4d1 · 420c4d1
1 parent 2f2c424
commit 420c4d1
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/rewriter b/rewriter
diff --git a/src/Language/APINotations.v b/src/Language/APINotations.v
@@ -5,6 +5,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Crypto.Language.PreExtra.
 Require Import Rewriter.Language.Language.
+Require Import Rewriter.Language.Reify.
 Require Import Crypto.Language.IdentifiersBasicGENERATED.
 Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
@@ -30,6 +31,7 @@ Import EqNotations.
 Module Compilers.
   Export Language.Pre.
   Export Language.Compilers.
+  Export Reify.Compilers.
   Import IdentifiersBasicLibrary.Compilers.
   Import IdentifiersBasicLibrary.Compilers.Basic.
   Import IdentifiersBasicGenerate.Compilers.Basic.Tactic.
+6 −0		.github/workflows/coq.yml
+1 −1		.github/workflows/docker-coq.yml
+2 −0		_CoqProject.in
+6 −4		src/Rewriter/Language/IdentifiersBasicGenerate.v
+0 −4		src/Rewriter/Language/IdentifiersLibrary.v
+0 −494		src/Rewriter/Language/Language.v
+544 −0		src/Rewriter/Language/Reify.v
+11 −3		src/Rewriter/Rewriter/Examples.v
+2 −0		src/Rewriter/Rewriter/Reify.v
+17 −14		src/Rewriter/Util/Tactics/CacheTerm.v
+10 −0		src/Rewriter/Util/Tactics/ClearFree.v