aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/cases.ml30
1 files changed, 21 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f21f0d5db..ab2529134 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -341,17 +341,29 @@ let inh_coerce_to_ind evdref env loc ty tyi =
un inductif cela doit être égal *)
if not (e_cumul env evdref expected_typ ty) then evdref := sigma
-let binding_vars_of_inductive = function
+let rec accumulate_bindings env t acc =
+ match kind_of_term t with
+ | App (f,v) when isConstruct f ->
+ let cstr,u = destConstruct f in
+ let n = constructor_nrealargs_env env cstr in
+ let l = List.lastn n (Array.to_list v) in
+ List.fold_right (accumulate_bindings env) l acc
+ | Rel _ | Var _ -> List.add_set Constr.equal t acc
+ | _ -> acc
+
+let binding_vars_of_inductive deep env = function
| NotInd _ -> []
- | IsInd (_,IndType(_,realargs),_) -> List.filter (fun c -> isRel c || isVar c) realargs
+ | IsInd (_,IndType(_,realargs),_) ->
+ if deep then List.fold_right (accumulate_bindings env) realargs []
+ else List.filter (fun c -> isRel c || isVar c) realargs
-let extract_inductive_data env sigma decl =
+let extract_inductive_data deep env sigma decl =
match decl with
| LocalAssum (_,t) ->
let tmtyp =
try try_find_ind env sigma t None
with Not_found -> NotInd (None,t) in
- let tmtypvars = binding_vars_of_inductive tmtyp in
+ let tmtypvars = binding_vars_of_inductive deep env tmtyp in
(tmtyp,tmtypvars)
| LocalDef (_,_,t) ->
(NotInd (None, t), [])
@@ -1286,7 +1298,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let typs' =
List.map (fun (c,d) ->
- (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in
+ (c,extract_inductive_data false extenv !(pb.evdref) d,d)) typs' in
(* We compute over which of x(i+1)..xn and x matching on xi will need a *)
(* generalization *)
@@ -1419,7 +1431,7 @@ and match_current pb (initial,tomatch) =
(* We compile branches *)
let brvals = Array.map2 (compile_branch initial current realargs (names,dep) deps pb arsign) eqns cstrs in
(* We build the (elementary) case analysis *)
- let depstocheck = current::binding_vars_of_inductive typ in
+ let depstocheck = current::binding_vars_of_inductive false pb.env typ in
let brvals,tomatch,pred,inst =
postprocess_dependencies !(pb.evdref) depstocheck
brvals pb.tomatch pb.pred deps cstrs in
@@ -1801,7 +1813,7 @@ let build_inversion_problem loc env sigma tms t =
let pb_env = push_rel_context sign env in
let decls =
- List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
+ List.map (fun (c,d) -> (c,extract_inductive_data false pb_env sigma d,d)) decls in
let decls = List.rev decls in
let dep_sign = find_dependencies_signature (List.make n true) decls in
@@ -2511,7 +2523,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
let typs =
- List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in
+ List.map (fun (c,d) -> (c,extract_inductive_data true env !evdref d,d)) typs in
let dep_sign =
find_dependencies_signature
@@ -2586,7 +2598,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
let typs =
- List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
+ List.map (fun (c,d) -> (c,extract_inductive_data true env sigma d,d)) typs in
let dep_sign =
find_dependencies_signature