aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r--tactics/tacticals.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f7a8a787c..b2d39b57a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -201,7 +201,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
let rec analrec c recargs =
match kind_of_term c, recargs with
| Prod (_,_,c), recarg::rest ->
- let b = match dest_recarg recarg with
+ let b = match Declareops.dest_recarg recarg with
| Norec | Imbr _ -> false
| Mrec (_,j) -> isrec && Int.equal j k
in b :: (analrec c rest)
@@ -213,7 +213,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
let n = mib.mind_nparams in
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
+ let lrecargs = Declareops.dest_subterms mip.mind_recargs in
Array.map2 analrec lc lrecargs
let elimination_sort_of_goal gl =