aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egrammar.ml6
-rw-r--r--parsing/g_ascii_syntax.ml2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/pcoq.ml44
-rw-r--r--parsing/ppconstr.ml8
-rw-r--r--parsing/ppvernac.ml4
-rw-r--r--parsing/prettyp.ml4
-rw-r--r--parsing/search.ml4
10 files changed, 20 insertions, 20 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index e28890cee7..b2c279b39c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -160,7 +160,7 @@ type grammar_tactic_production =
let make_prod_item = function
| TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
- | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po)
+ | TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po)
(* Tactic grammar extensions *)
@@ -194,7 +194,7 @@ let extend_vernac_command_grammar s gl =
let find_index s t =
let t,n = repr_ident (id_of_string t) in
if s <> t or n = None then raise Not_found;
- out_some n
+ Option.get n
let rec interp_entry_name up_level s =
let l = String.length s in
@@ -233,7 +233,7 @@ let make_vprod_item n = function
| VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
| VNonTerm (loc, nt, po) ->
let (etyp, e) = interp_entry_name n nt in
- e, option_map (fun p -> (p,etyp)) po
+ e, Option.map (fun p -> (p,etyp)) po
let get_tactic_entry n =
if n = 0 then
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index ac54fc63d5..717abaa66a 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -72,7 +72,7 @@ let make_ascii_string n =
if n>=32 && n<=126 then String.make 1 (char_of_int n)
else Printf.sprintf "%03d" n
-let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
let _ =
Notation.declare_string_interpreter "char_scope"
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 04e0f84ca3..4627d23052 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -59,7 +59,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
(snd id,(n,ro),bl,ty,body)
let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
- let _ = option_map (fun (aloc,_) ->
+ let _ = Option.map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofixb",
Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9b21837d8b..23e4ba6218 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -104,7 +104,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
(id,n,CProdN(loc,bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
- let _ = option_map (fun (aloc,_) ->
+ let _ = Option.map (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofix_tac",
Pp.str"Annotation forbidden in cofix expression")) ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a64cf74cc7..a7a78f7700 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -274,8 +274,8 @@ GEXTEND Gram
;
rec_annotation:
[ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
- | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel)
- | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel)
+ | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel)
+ | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel)
| -> (None, CStructRec)
] ]
;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d72a490467..07055869af 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -576,7 +576,7 @@ let find_position forpat other assoc lev =
| (p,_ as pa)::l when p > n -> pa :: add_level (Some p) l
| (p,a)::l when p = n ->
if admissible_assoc (a,assoc) then raise Exit;
- error_level_assoc p a (out_some assoc)
+ error_level_assoc p a (Option.get assoc)
| l -> after := q; (n,create_assoc assoc)::l
in
try
@@ -587,7 +587,7 @@ let find_position forpat other assoc lev =
level_stack := updated:: !level_stack;
let assoc = create_assoc assoc in
(if !after = None then Some Gramext.First
- else Some (Gramext.After (constr_level (out_some !after)))),
+ else Some (Gramext.After (constr_level (Option.get !after)))),
Some assoc, Some (constr_level n)
with
Exit ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 1c9eb1e2a2..8e542ce147 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -386,12 +386,12 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
match ro with
CStructRec ->
if List.length ids > 1 && n <> None then
- spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+ spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
else mt()
| CWfRec c ->
- spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+ spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
| CMeasureRec c ->
- spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
+ spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
@@ -428,7 +428,7 @@ let pr_case_item pr (tm,(na,indnalopt)) =
| Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id
| Anonymous when tm_clash (tm,indnalopt) <> None ->
(* hide [tm] name to avoid conflicts *)
- spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*)
+ spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*)
| _ -> mt ()) ++
*)
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a5bcea6f1b..bbb481f3e2 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 ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index a2341edb1e..a3a0c2f152 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -456,10 +456,10 @@ let gallina_print_leaf_entry with_values c =
let gallina_print_context with_values =
let rec prec n = function
- | h::rest when n = None or out_some n > 0 ->
+ | h::rest when n = None or Option.get n > 0 ->
(match gallina_print_library_entry with_values h with
| None -> prec n rest
- | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
+ | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
| _ -> mt ()
in
prec
diff --git a/parsing/search.ml b/parsing/search.ml
index b9982ad3d2..fd9eb12bbb 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -52,7 +52,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
(try
let (idc,_,typ) = get_variable (basename sp) in
if refopt = None
- || head_const typ = constr_of_global (out_some refopt)
+ || head_const typ = constr_of_global (Option.get refopt)
then
fn (VarRef idc) env typ
with Not_found -> (* we are in a section *) ())
@@ -60,7 +60,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
let cst = locate_constant (qualid_of_sp sp) in
let typ = Typeops.type_of_constant env cst in
if refopt = None
- || head_const typ = constr_of_global (out_some refopt)
+ || head_const typ = constr_of_global (Option.get refopt)
then
fn (ConstRef cst) env typ
| "INDUCTIVE" ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 08:52:12 +0000