From 7ad15b924fa920a354eff74fe85b73e499e8af3a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Apr 2017 19:31:04 -0400 Subject: Split up Compilers/Z/Bounds/InterpretationLemmas --- _CoqProject | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 07a1305b8..dba0fdcf4 100644 --- a/_CoqProject +++ b/_CoqProject @@ -131,13 +131,15 @@ src/Compilers/Z/OpInversion.v src/Compilers/Z/Reify.v src/Compilers/Z/Syntax.v src/Compilers/Z/Bounds/Interpretation.v -src/Compilers/Z/Bounds/InterpretationLemmas.v src/Compilers/Z/Bounds/MapCastByDeBruijn.v src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v src/Compilers/Z/Bounds/Pipeline.v src/Compilers/Z/Bounds/Relax.v src/Compilers/Z/Bounds/RoundUpLemmas.v +src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v +src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v src/Compilers/Z/Bounds/Pipeline/Definition.v src/Compilers/Z/Bounds/Pipeline/Glue.v src/Compilers/Z/Bounds/Pipeline/OutputType.v -- cgit v1.2.3