diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 10:12:00 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 10:12:00 +0100 |
| commit | 9accca23fb79f8a14d1cd35fa681a2e0bece1db5 (patch) | |
| tree | e2f20c83834e9956e59e0a8144e93ed4af7392b2 /pretyping | |
| parent | 08cbbdbcdf3456b9e1a0e688b13f431a946f3bad (diff) | |
| parent | 20916bd558a355b597337101e3281bb5ebbfcd36 (diff) | |
Merge PR #6759: detype_case predicate is not optional
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 22 |
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 |