diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bfbce8f6eb..ec8d4d0e14 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -20,6 +20,7 @@ open Tacmach open Clenv open Tactypes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (************************************************************************) @@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = - match Constr.kind c, recargs with - | Prod (_,_,c), recarg::rest -> + match c, recargs with + | RelDecl.LocalAssum _ :: c, recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest @@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end - | LetIn (_,_,_,c), rest -> false :: analrec c rest - | _, [] -> [] + | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest + | [], [] -> [] | _ -> anomaly (Pp.str "compute_constructor_signatures.") in let (mib,mip) = Global.lookup_inductive ity in - let n = mib.mind_nparams in - let lc = - Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in + let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in + let lc = Array.map map mip.mind_nf_lc in let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs |