diff options
| author | vblot <24938579+vblot@users.noreply.github.com> | 2021-09-08 11:57:46 +0200 |
|---|---|---|
| committer | vblot <24938579+vblot@users.noreply.github.com> | 2021-09-08 11:57:46 +0200 |
| commit | dd39cc1bac964130e8738472c89f07786cfa90c6 (patch) | |
| tree | 295a1655970bbc14374734bde6286c4bfeeee72f | |
| parent | 956c3c4681967107cdf682432ce5c90553af000b (diff) | |
| parent | f513d4d2e04c4bbce3c5a40219bb89dbc57eed26 (diff) | |
| download | smtcoq-dd39cc1bac964130e8738472c89f07786cfa90c6.tar.gz smtcoq-dd39cc1bac964130e8738472c89f07786cfa90c6.zip | |
Merge remote-tracking branch 'coq-8.10' into coq-8.11
| -rw-r--r-- | src/trace/smtAtom.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 78f2eee..3e16f6c 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 = CoqInterface.retyping_get_type_of env sigma x in - if Constr.iskind ty || - let c, _ = CoqInterface.decompose_app ty in - CoqInterface.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 = CoqInterface.retyping_get_type_of env sigma x in + if Constr.iskind ty || + let c, _ = CoqInterface.decompose_app ty in + CoqInterface.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 = |