aboutsummaryrefslogtreecommitdiffstats
path: root/_CoqProject
diff options
context:
space:
mode:
authorJames Pollard <james@pollard.dev>2020-06-14 16:41:27 +0100
committerJames Pollard <james@pollard.dev>2020-06-14 16:41:27 +0100
commit044a68b1b215125e2651c637f28c794536d27ba5 (patch)
tree53c0a4c94b048fa1f96d7cdf3ef73169b6fe2398 /_CoqProject
parent39d438f9c2b3d1484ae0e2afe33a19c2f654a8b0 (diff)
downloadvericert-kvx-044a68b1b215125e2651c637f28c794536d27ba5.tar.gz
vericert-kvx-044a68b1b215125e2651c637f28c794536d27ba5.zip
Array semantics now uses dependent Array type.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject
index a1026ed..7965da9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,4 +14,4 @@
-R lib/CompCert/flocq compcert.flocq
-R lib/CompCert/lib compcert.lib
-R lib/CompCert/x86 compcert.x86
--R lib/CompCert/x86_32 compcert.x86_64
+-R lib/CompCert/x86_32 compcert.x86_32