aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtAtom.ml')
-rw-r--r--src/trace/smtAtom.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 3e16f6c..9697882 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1351,7 +1351,7 @@ module Atom =
let c, _ = CoqInterface.decompose_app ty in
CoqInterface.eq_constr c (Lazy.force cCompDec)
then
- (x::[], xs)
+ ([x], xs)
else
([], l)
| _ -> (x::l1, l2)