diff options
author | 2018-08-06 11:16:57 -0400 | |
---|---|---|
committer | 2018-08-06 14:30:15 -0400 | |
commit | a8015c7f9e176fba282052c13fe69cb53da939dd (patch) | |
tree | 399240aa999505af78816239501aabbc1f817269 /src/Experiments/NewPipeline/Toplevel1.v | |
parent | edb9da3f52088caae86636393287071317d4a51c (diff) |
Start setting up abs-int interp proofs
Diffstat (limited to 'src/Experiments/NewPipeline/Toplevel1.v')
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 437855405..3b8f81ac6 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -52,6 +52,7 @@ Require Crypto.Experiments.NewPipeline.LanguageWf. Require Crypto.Experiments.NewPipeline.UnderLetsProofs. Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs. Require Crypto.Experiments.NewPipeline.RewriterProofs. +Require Crypto.Experiments.NewPipeline.AbstractInterpretationWf. Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope Z_scope. @@ -499,6 +500,7 @@ Import Crypto.Experiments.NewPipeline.UnderLetsProofs Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs Crypto.Experiments.NewPipeline.RewriterProofs + Crypto.Experiments.NewPipeline.AbstractInterpretationWf Crypto.Experiments.NewPipeline.AbstractInterpretationProofs Crypto.Experiments.NewPipeline.Language Crypto.Experiments.NewPipeline.UnderLets @@ -512,6 +514,7 @@ Import UnderLetsProofs.Compilers MiscCompilerPassesProofs.Compilers RewriterProofs.Compilers + AbstractInterpretationWf.Compilers AbstractInterpretationProofs.Compilers Language.Compilers UnderLets.Compilers |