From 9f4911d5a10d06b2a78262c0ba81a1540570c56c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 Oct 2018 19:24:29 -0400 Subject: Refactor/generalize some pipeline definitions/proofs When we do rewriting after casts, we will need to do extra passes of DCE and subst01 to fully reduce things, so we generalize some of the interp proofs over cast behavior. For ease of rewriting, we make [ident.interp] an alias (notation) for [ident.gen_interp], rather than a [Definition]. We also factor out the rewriting wrapper inside the pipeline module into its own definition. --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index 51f1d10ce..a832118d6 100644 --- a/.gitignore +++ b/.gitignore @@ -45,6 +45,8 @@ nra.cache /time-of-build-pretty.log /time-of-build.log +/*.out + # compilation outputs /*.o etc/tscfreq -- cgit v1.2.3