diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a5bcea6f1..bbb481f3e 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -747,7 +747,7 @@ let rec pr_vernac = function prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ str" :=" ++ brk(1,1) ++ - let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in + let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in pr_raw_tactic_env (idl @ List.map snd (List.map fst l)) (Global.env()) @@ -794,7 +794,7 @@ let rec pr_vernac = function spc() ++ str"in" ++ spc () ++ pr_constr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) in - (if io = None then mt() else int (out_some io) ++ str ": ") ++ + (if io = None then mt() else int (Option.get io) ++ str ": ") ++ pr_mayeval r c | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) | VernacPrint p -> |