diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 015c26531a..870b96813d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -599,7 +599,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk ((id,c)::subst, update, sigma) in let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in check_instance loc subst inst; - sigma, Array.map_of_list snd subst + sigma, List.map snd subst module Default = struct |