aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-08-30 16:36:28 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2021-08-30 16:36:28 +0200
commit9f2ad0d53d9a26a6f12d35ec43cfbd412cfdee2f (patch)
treea0269b2bfb73ec9ac0f7094daff4d277d44bd420
parentf4bed7efd425a692661606cd1df239bd507e594f (diff)
parenta8863500307f01b9df6d13b19db61066d219c553 (diff)
downloadsmtcoq-9f2ad0d53d9a26a6f12d35ec43cfbd412cfdee2f.tar.gz
smtcoq-9f2ad0d53d9a26a6f12d35ec43cfbd412cfdee2f.zip
Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11
-rw-r--r--src/PArray/PArray.v (renamed from src/Array/PArray.v)0
-rw-r--r--src/_CoqProject4
-rw-r--r--src/trace/coqInterface.ml2
3 files changed, 3 insertions, 3 deletions
diff --git a/src/Array/PArray.v b/src/PArray/PArray.v
index 35d68b4..35d68b4 100644
--- a/src/Array/PArray.v
+++ b/src/PArray/PArray.v
diff --git a/src/_CoqProject b/src/_CoqProject
index 41e0306..9ac5799 100644
--- a/src/_CoqProject
+++ b/src/_CoqProject
@@ -28,10 +28,10 @@
-I trace
-I verit
-I zchaff
--I Array
+-I PArray
-I ../3rdparty/alt-ergo
-Array/PArray.v
+PArray/PArray.v
bva/BVList.v
bva/Bva_checker.v
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml
index d1914cc..5aa1087 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -110,7 +110,7 @@ let cint = gen_constant int63_module "int"
(* PArray *)
-let parray_modules = [["SMTCoq";"Array";"PArray"]]
+let parray_modules = [["SMTCoq";"PArray";"PArray"]]
let cmake = gen_constant parray_modules "make"
let cset = gen_constant parray_modules "set"