diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 752819aa3..c93b1e568 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) +let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = @@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs = let nal,c = it_destRLambda_or_LetIn_names n b in let mkPatVar na = CAst.make @@ PatVar na in let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let map name = try Some (Nameops.out_name name) with Failure _ -> None in - let ids = List.map_filter map nal in + let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs |