diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:02:36 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-06-21 15:03:39 -0400 |
| commit | b8f07f2bb73ea9691c642fd9b32d623bda9b6780 (patch) | |
| tree | 4c07572b09020060c93389bfb807f91bb3d53b08 /_CoqProject | |
| parent | ac478e7dc72df91dd51586c345ac4c329f644b14 (diff) | |
src/Demo.v: a 200-line introduction to BaseSystem ideas
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 7819439ff..c4f414b6c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,6 +3,7 @@ -arg "-compat 8.6" Bedrock/Nomega.v Bedrock/Word.v +src/Demo.v src/Algebra/Field.v src/Algebra/Field_test.v src/Algebra/Group.v @@ -276,6 +277,7 @@ src/Util/Option.v src/Util/PartiallyReifiedProp.v src/Util/PointedProp.v src/Util/Prod.v +src/Util/QUtil.v src/Util/Relations.v src/Util/Sigma.v src/Util/Sum.v @@ -287,6 +289,7 @@ src/Util/Unit.v src/Util/WordUtil.v src/Util/ZRange.v src/Util/ZUtil.v +src/Util/Decidable/Bool2Prop.v src/Util/ForLoop/Instances.v src/Util/ForLoop/InvariantFramework.v src/Util/ForLoop/Tests.v |