aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-05 13:39:13 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-14 15:39:28 +0100
commit20916bd558a355b597337101e3281bb5ebbfcd36 (patch)
tree06946e7bb2f8928872ae4e18c945e7c3443dca8d
parentd2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff)
detype_case predicate is not optional
-rw-r--r--pretyping/detyping.ml22
1 files changed, 10 insertions, 12 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 754e88139..18ecbf8ed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -451,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
then
Anonymous, None, None
else
- match Option.map detype p with
- | None -> Anonymous, None, None
- | Some p ->
- let nl,typ = it_destRLambda_or_LetIn_names k p in
- let n,typ = match DAst.get typ with
- | GLambda (x,_,t,c) -> x, c
- | _ -> Anonymous, typ in
- let aliastyp =
- if List.for_all (Name.equal Anonymous) nl then None
- else Some (Loc.tag (indsp,nl)) in
- n, aliastyp, Some typ
+ let p = detype p in
+ let nl,typ = it_destRLambda_or_LetIn_names k p in
+ let n,typ = match DAst.get typ with
+ | GLambda (x,_,t,c) -> x, c
+ | _ -> Anonymous, typ in
+ let aliastyp =
+ if List.for_all (Name.equal Anonymous) nl then None
+ else Some (Loc.tag (indsp,nl)) in
+ n, aliastyp, Some typ
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
let tag =
@@ -650,7 +648,7 @@ and detype_r d flags avoid env sigma t =
(is_nondep_branch sigma) avoid
(ci.ci_ind,ci.ci_pp_info.style,
ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
- (Some p) c bl
+ p c bl
| Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
| CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef