diff options
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index d7d304279..49eab5d29 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -159,7 +159,7 @@ let list_of_local_binders l = let lift_binders k n l = let rec aux n = function - | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl + | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl | [] -> [] in aux n l @@ -326,7 +326,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> - (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx + (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx let build_mutrec lnameargsardef boxed = let sigma = Evd.empty and env = Global.env () in |