aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtBtype.ml
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2022-02-15 18:34:33 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2022-02-15 18:34:33 +0100
commit23ac3ceceb92cdbc2026253c1bae388a2b9b6e18 (patch)
tree8409e89bf143ff9b97474b7ead6bb2aaf4f934eb /src/trace/smtBtype.ml
parent81b13b26f6dabca0152a9244fc474cd8ecb29905 (diff)
parent761a4af555c228a9fdd34ae33f9c842931a592cf (diff)
downloadsmtcoq-23ac3ceceb92cdbc2026253c1bae388a2b9b6e18.tar.gz
smtcoq-23ac3ceceb92cdbc2026253c1bae388a2b9b6e18.zip
Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12
Diffstat (limited to 'src/trace/smtBtype.ml')
-rw-r--r--src/trace/smtBtype.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index c610129..923874e 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -156,7 +156,7 @@ let interp_tbl reify =
| _ -> Some bt
in
Hashtbl.filter_map_inplace set reify.tbl;
- CoqInterface.mkArray (Lazy.force ctyp_compdec, t)
+ CoqTerms.mkArray (Lazy.force ctyp_compdec, t)
let to_list reify =