From ad5ddae0406770990bc43bc10cc753470c7e27af Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Wed, 8 Sep 2021 11:25:50 +0200
Subject: generalize polymorphic arguments detection

---
 src/trace/smtAtom.ml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 2710eb2..1d608e6 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1343,15 +1343,18 @@ module Atom =
         let rec collect_types = function
           | [] -> ([],[])
           | x::xs as l ->
-             let ty = Structures.retyping_get_type_of env sigma x in
-             if Constr.iskind ty ||
-                  let c, _ = Structures.decompose_app ty in
-                  Structures.eq_constr c (Lazy.force cCompDec)
-             then
-               let (l1, l2) = collect_types xs in
-               (x::l1, l2)
-             else
-               ([], l)
+             let (l1, l2) = collect_types xs in
+             match l1 with
+               | [] -> 
+                 let ty = Structures.retyping_get_type_of env sigma x in
+                 if Constr.iskind ty ||
+                      let c, _ = Structures.decompose_app ty in
+                      Structures.eq_constr c (Lazy.force cCompDec)
+                 then
+                   (x::[], xs)
+                 else
+                   ([], l)
+               | _ -> (x::l1, l2)
         in
         let (args1, args2) = collect_types args in
         let c, args =
-- 
cgit