diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-10-14 17:07:25 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-10-14 17:07:25 +0200 |
| commit | abe0badbe84a90bae4f20541781609ed0ebb3fb9 (patch) | |
| tree | 9ef79ba157b4b1ba20c89903a88454a3babbe341 | |
| parent | 38227d031b7b5d22fd1dfba0c250d9d176659d44 (diff) | |
| download | smtcoq-abe0badbe84a90bae4f20541781609ed0ebb3fb9.tar.gz smtcoq-abe0badbe84a90bae4f20541781609ed0ebb3fb9.zip | |
Small optim
| -rw-r--r-- | src/trace/smtAtom.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 1d608e6..06e1472 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1351,7 +1351,7 @@ module Atom = let c, _ = Structures.decompose_app ty in Structures.eq_constr c (Lazy.force cCompDec) then - (x::[], xs) + ([x], xs) else ([], l) | _ -> (x::l1, l2) |