From 805ef6e2c439544eabc1c54d5901050d0f6e934b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 13 Jun 2017 18:59:45 -0400 Subject: Stronger invert_op tactic Now it can handle ops that return (Tbase TZ) --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index caefd076d..d5fddbc2a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -143,6 +143,7 @@ src/Compilers/Z/RewriteAddToAdc.v src/Compilers/Z/RewriteAddToAdcInterp.v src/Compilers/Z/RewriteAddToAdcWf.v src/Compilers/Z/Syntax.v +src/Compilers/Z/TypeInversion.v src/Compilers/Z/Bounds/Interpretation.v src/Compilers/Z/Bounds/MapCastByDeBruijn.v src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v -- cgit v1.2.3