diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f88530eec..637269a66 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -211,7 +211,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let lc = Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in let lrecargs = dest_subterms mip.mind_recargs in - array_map2 analrec lc lrecargs + Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = pf_apply Retyping.get_sort_family_of gl (pf_concl gl) |