diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 10 | ||||
| -rw-r--r-- | toplevel/minicoq.ml | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 28 |
6 files changed, 23 insertions, 23 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 933b23c53e..7546ad310b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -321,7 +321,7 @@ let init is_ide = set_vm_opt (); engage (); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then - option_iter Declaremods.start_library !toplevel_name; + Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e25ff99e0c..bb30c669fc 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,7 +320,7 @@ let explain_hole_kind env = function | BinderType Anonymous -> str "the type of this anonymous binder" | ImplicitArg (c,(n,ido)) -> - let id = out_some ido in + let id = Option.get ido in str "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 9a162997b6..7ebf3dfa9a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -763,21 +763,21 @@ let find_precedence lev etyps symbols = | ETPattern | ETOther _ -> (* Give a default ? *) if lev = None then error "Need an explicit level" - else out_some lev + else Option.get lev | ETConstrList _ -> assert false (* internally used in grammar only *) with Not_found -> if lev = None then error "A left-recursive notation must have an explicit level" - else out_some lev) + else Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then (Options.if_verbose msgnl (str "Setting notation at level 0"); 0) - else out_some lev + else Option.get lev | _ -> if lev = None then error "Cannot determine the level"; - out_some lev + Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () @@ -839,7 +839,7 @@ let compute_syntax_data (df,modifiers) = (* Registration of notations interpretation *) let load_notation _ (_,(_,scope,pat,onlyparse,_)) = - option_iter Notation.declare_scope scope + Option.iter Notation.declare_scope scope let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 19fd343e57..e22b33e24c 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -54,7 +54,7 @@ let check c = let definition id ty c = let c = globalize [] c in - let ty = option_map (globalize []) ty in + let ty = Option.map (globalize []) ty in let ce = { const_entry_body = c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce (locals()) !env; diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index fbdc96d6e8..aba5aeb274 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -103,7 +103,7 @@ let get_bols_of_loc ibuf (bp,ep) = lines_rec ll nafter fl in let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in - (fl,out_some ll) + (fl,Option.get ll) let dotted_location (b,e) = if e-b < 3 then diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d6b874c228..9cb2b26b73 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -298,7 +298,7 @@ let vernac_notation = Metasyntax.add_notation let start_proof_and_print idopt k t hook = start_proof_com idopt k t hook; print_subgoals (); - if !pcoq <> None then (out_some !pcoq).start_proof () + if !pcoq <> None then (Option.get !pcoq).start_proof () let vernac_definition (local,_,_ as k) id def hook = match def with @@ -386,7 +386,7 @@ let vernac_declare_module export id binders_ast mty_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast (Some mty_ast_o) None; if_verbose message ("Module "^ string_of_id id ^" is declared"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) @@ -406,7 +406,7 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = ("Interactive Module "^ string_of_id id ^" started") ; List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport | Some _ -> @@ -422,13 +422,13 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = id binders_ast mty_ast_o mexpr_ast_o; if_verbose message ("Module "^ string_of_id id ^" is defined"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_end_module export id = Declaremods.end_module id; if_verbose message ("Module "^ string_of_id id ^" is defined") ; - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_declare_module_type id binders_ast mty_ast_o = @@ -447,7 +447,7 @@ let vernac_declare_module_type id binders_ast mty_ast_o = ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport @@ -542,7 +542,7 @@ let vernac_solve n tcom b = reset_top_of_script () end; print_subgoals(); - if !pcoq <> None then (out_some !pcoq).solve n + if !pcoq <> None then (Option.get !pcoq).solve n (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -910,12 +910,12 @@ let vernac_check_may_eval redexp glopt rc = let j = Typeops.typing env c in match redexp with | None -> - if !pcoq <> None then (out_some !pcoq).print_check env j + if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in if !pcoq <> None - then (out_some !pcoq).print_eval redfun env evmap rc j + then (Option.get !pcoq).print_eval redfun env evmap rc j else msg (print_eval redfun env evmap rc j) (* The same but avoiding the current goal context if any *) @@ -940,7 +940,7 @@ let vernac_print = function | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> - if !pcoq <> None then (out_some !pcoq).print_name qid + if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) @@ -995,7 +995,7 @@ let interp_search_about_item = function let vernac_search s r = let r = interp_search_restriction r in - if !pcoq <> None then (out_some !pcoq).search s r else + if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in @@ -1034,12 +1034,12 @@ let vernac_abort = function | None -> delete_current_proof (); if_verbose message "Current goal aborted"; - if !pcoq <> None then (out_some !pcoq).abort "" + if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); - if !pcoq <> None then (out_some !pcoq).abort s + if !pcoq <> None then (Option.get !pcoq).abort s let vernac_abort_all () = if refining() then begin @@ -1109,7 +1109,7 @@ let explain_tree occ = let vernac_show = function | ShowGoal nopt -> - if !pcoq <> None then (out_some !pcoq).show_goal nopt + if !pcoq <> None then (Option.get !pcoq).show_goal nopt else msg (match nopt with | None -> pr_open_subgoals () | Some n -> pr_nth_open_subgoal n) |