aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml16
-rw-r--r--pretyping/clenv.ml4
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/detyping.ml18
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/evd.ml2
-rw-r--r--pretyping/matching.ml2
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/rawterm.ml10
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--pretyping/tacred.ml2
13 files changed, 40 insertions, 42 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fd8f24370a..058f3d210d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -421,7 +421,7 @@ let mkDeclTomatch na = function
let map_tomatch_type f = function
| IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
- | NotInd (c,t) -> NotInd (option_map f c, f t)
+ | NotInd (c,t) -> NotInd (Option.map f c, f t)
let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -1139,7 +1139,7 @@ let rec generalize_problem pb = function
let tomatch = regeneralize_index_tomatch (i+1) tomatch in
{ pb with
tomatch = Abstract d :: tomatch;
- pred = option_map (generalize_predicate i d) pb'.pred }
+ pred = Option.map (generalize_predicate i d) pb'.pred }
(* No more patterns: typing the right-hand-side of equations *)
let build_leaf pb =
@@ -1154,7 +1154,7 @@ let build_leaf pb =
let shift_problem (current,t) pb =
{pb with
tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
- pred = option_map (specialize_predicate_var (current,t)) pb.pred;
+ pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
history = push_history_pattern 0 AliasLeaf pb.history;
mat = List.map remove_current_pattern pb.mat }
@@ -1224,7 +1224,7 @@ let build_branch current deps pb eqns const_info =
{ pb with
env = push_rels sign pb.env;
tomatch = List.rev_append currents tomatch;
- pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
+ pred = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
history = history;
mat = List.map (push_rels_eqn_with_names sign) submat }
@@ -1291,7 +1291,7 @@ and compile_generalization pb d rest =
{ pb with
env = push_rel d pb.env;
tomatch = rest;
- pred = option_map ungeneralize_predicate pb.pred;
+ pred = Option.map ungeneralize_predicate pb.pred;
mat = List.map (push_rels_eqn [d]) pb.mat } in
let j = compile pb in
{ uj_val = mkLambda_or_LetIn d j.uj_val;
@@ -1316,7 +1316,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
{pb with
env = newenv;
tomatch = tomatch;
- pred = option_map (lift_predicate n) pb.pred;
+ pred = Option.map (lift_predicate n) pb.pred;
history = history;
mat = mat } in
let j = compile pb in
@@ -1500,7 +1500,7 @@ let extract_arity_signature env0 tomatchl tmsign =
match tm with
| NotInd (bo,typ) ->
(match t with
- | None -> [na,option_map (lift n) bo,lift n typ]
+ | None -> [na,Option.map (lift n) bo,lift n typ]
| Some (loc,_,_,_) ->
user_err_loc (loc,"",
str "Unexpected type annotation for a term of non inductive type"))
@@ -1566,7 +1566,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
let allnames = List.rev (List.map (List.map pi1) arsign) in
let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
let _ =
- option_map (fun tycon ->
+ Option.map (fun tycon ->
evdref := Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val
(lift_tycon_type (List.length arsign) tycon))
tycon
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index dbc51514c1..b9881aaf04 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -106,7 +106,7 @@ let clenv_environments evd bound t =
let dep = dependent (mkRel 1) t2 in
let na' = if dep then na else Anonymous in
let e' = meta_declare mv t1 ~name:na' e in
- clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
+ clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
| (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
| (n, _) -> (e, List.rev metas, t)
@@ -124,7 +124,7 @@ let clenv_environments_evars env evd bound t =
| (n, Prod (na,t1,t2)) ->
let e',constr = Evarutil.new_evar e env t1 in
let dep = dependent (mkRel 1) t2 in
- clrec (e', constr::ts) (option_map ((+) (-1)) n)
+ clrec (e', constr::ts) (Option.map ((+) (-1)) n)
(if dep then (subst1 constr t2) else t2)
| (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
| (n, _) -> (e, List.rev ts, t)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 62e29dc066..f3468bcbf1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -184,7 +184,7 @@ module Default = struct
kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
with
| Prod (_,t1,t2), Prod (name,u1,u2) ->
- let v' = option_map (whd_betadeltaiota env (evars_of evd)) v in
+ let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in
let (evd',b) =
match v' with
| Some v' ->
@@ -201,7 +201,7 @@ module Default = struct
let env1 = push_rel (x,None,v1) env in
let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
(Some v2) t2 u2 in
- (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2',
+ (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2',
mkProd (x, v1, t2'))
| None ->
(* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
@@ -219,7 +219,7 @@ module Default = struct
let (evd'', v2', t2') =
let v2 =
match v with
- | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+ | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1'
| None -> None
and evd', t2 =
match v1' with
@@ -231,7 +231,7 @@ module Default = struct
in
inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
in
- (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+ (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2',
mkProd (name, u1, t2')))
| _ -> raise NoCoercion
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 829c5f4048..9dfe393bea 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -303,7 +303,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
then
Anonymous, None, None
else
- match option_map detype p with
+ match Option.map detype p with
| None -> Anonymous, None, None
| Some p ->
let nl,typ = it_destRLambda_or_LetIn_names k p in
@@ -340,7 +340,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
if array_for_all ((<>) None) nondepbrs then
RIf (dl,tomatch,(alias,pred),
- out_some nondepbrs.(0),out_some nondepbrs.(1))
+ Option.get nondepbrs.(0),Option.get nondepbrs.(1))
else
RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
| _ ->
@@ -529,7 +529,7 @@ and detype_binder isgoal bk avoid env na ty c =
| BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
let rec detype_rel_context where avoid env sign =
- let where = option_map (fun c -> it_mkLambda_or_LetIn c sign) where in
+ let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
let rec aux avoid env = function
| [] -> []
| (na,b,t)::rest ->
@@ -539,7 +539,7 @@ let rec detype_rel_context where avoid env sign =
| Some c ->
if b<>None then concrete_let_name None avoid env na c
else concrete_name None avoid env na c in
- let b = option_map (detype false avoid env) b in
+ let b = Option.map (detype false avoid env) b in
let t = detype false avoid env t in
(na',b,t) :: aux avoid' (add_name na' env) rest
in aux avoid env (List.rev sign)
@@ -589,11 +589,11 @@ let rec subst_rawconstr subst raw =
RLetIn (loc,n,r1',r2')
| RCases (loc,rtno,rl,branches) ->
- let rtno' = option_smartmap (subst_rawconstr subst) rtno
+ let rtno' = Option.smartmap (subst_rawconstr subst) rtno
and rl' = list_smartmap (fun (a,x as y) ->
let a' = subst_rawconstr subst a in
let (n,topt) = x in
- let topt' = option_smartmap
+ let topt' = Option.smartmap
(fun (loc,(sp,i),x,y as t) ->
let sp' = subst_kn subst sp in
if sp == sp' then t else (loc,(sp',i),x,y)) topt in
@@ -611,14 +611,14 @@ let rec subst_rawconstr subst raw =
RCases (loc,rtno',rl',branches')
| RLetTuple (loc,nal,(na,po),b,c) ->
- let po' = option_smartmap (subst_rawconstr subst) po
+ let po' = Option.smartmap (subst_rawconstr subst) po
and b' = subst_rawconstr subst b
and c' = subst_rawconstr subst c in
if po' == po && b' == b && c' == c then raw else
RLetTuple (loc,nal,(na,po'),b',c')
| RIf (loc,c,(na,po),b1,b2) ->
- let po' = option_smartmap (subst_rawconstr subst) po
+ let po' = Option.smartmap (subst_rawconstr subst) po
and b1' = subst_rawconstr subst b1
and b2' = subst_rawconstr subst b2
and c' = subst_rawconstr subst c in
@@ -631,7 +631,7 @@ let rec subst_rawconstr subst raw =
let bl' = array_smartmap
(list_smartmap (fun (na,obd,ty as dcl) ->
let ty' = subst_rawconstr subst ty in
- let obd' = option_smartmap (subst_rawconstr subst) obd in
+ let obd' = Option.smartmap (subst_rawconstr subst) obd in
if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
bl in
if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9d0ae75e70..93e1c11576 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -43,7 +43,7 @@ let eval_flexible_term env c =
match kind_of_term c with
| Const c -> constant_opt_value env c
| Rel n ->
- (try let (_,v,_) = lookup_rel n env in option_map (lift n) v
+ (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
with Not_found -> None)
| Var id ->
(try let (_,v,_) = lookup_named id env in v with Not_found -> None)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cb64fcb561..1f256b3bda 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -226,7 +226,7 @@ let push_rel_context_to_named_context env typ =
Sign.fold_rel_context
(fun (na,c,t) (subst, avoid, env) ->
let id = next_name_away na avoid in
- let d = (id,option_map (substl subst) c,substl subst t) in
+ let d = (id,Option.map (substl subst) c,substl subst t) in
(mkVar id :: subst, id::avoid, push_named d env))
(rel_context env) ~init:([], ids, env) in
(named_context_val env, substl subst typ, inst_rels@inst_vars)
@@ -1133,7 +1133,7 @@ let lift_abstr_tycon_type n (abs, t) =
else (Some (init, abs'), t)
let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = option_map (lift_tycon_type n)
+let lift_tycon n = Option.map (lift_tycon_type n)
let pr_tycon_type env (abs, t) =
match abs with
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d0cbeb574c..6d75dada67 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -430,7 +430,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
if filter = None then
List.map (fun _ -> true) (named_context_of_val hyps)
else
- (let filter = out_some filter in
+ (let filter = Option.get filter in
assert (List.length filter = List.length (named_context_of_val hyps));
filter)
in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index cac06d2408..9ce8e703fe 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -153,7 +153,7 @@ let matches_core convert allow_partial_app pat c =
sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
| PRef (ConstRef _ as ref), _ when convert <> None ->
- let (env,evars) = out_some convert in
+ let (env,evars) = Option.get convert in
let c = constr_of_global ref in
if is_conv env evars c cT then sigma
else raise PatternMatchingFailure
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index c3b49b9749..d64e84fea0 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -185,7 +185,7 @@ let rec subst_pattern subst pat = match pat with
if c' == c && c1' == c1 && c2' == c2 then pat else
PIf (c',c1',c2')
| PCase ((a,b,ind,n as cs),typ,c,branches) ->
- let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+ let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in
let typ' = subst_pattern subst typ in
let c' = subst_pattern subst c in
let branches' = array_smartmap (subst_pattern subst) branches in
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 26ccc8024b..ad4e06a55a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,7 +60,7 @@ let env_ise sigma env =
Sign.fold_rel_context
(fun (na,b,ty) e ->
push_rel
- (na, option_map (nf_evar sigma) b, nf_evar sigma ty)
+ (na, Option.map (nf_evar sigma) b, nf_evar sigma ty)
e)
ctxt
~init:env0
@@ -76,7 +76,7 @@ let contract env lc =
env
| _ ->
let t' = substl !l t in
- let c' = option_map (substl !l) c in
+ let c' = Option.map (substl !l) c in
let na' = named_hd env t' na in
l := (mkRel 1) :: List.map (lift 1) !l;
push_rel (na',c',t') env in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 63e40a0521..d2a3473632 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -101,7 +101,7 @@ let cases_predicate_names tml =
- boolean in POldCase means it is recursive
i*)
-let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty)
+let map_rawdecl f (na,obd,ty) = (na,Option.map f obd,f ty)
let map_rawconstr f = function
| RVar (loc,id) -> RVar (loc,id)
@@ -110,13 +110,13 @@ let map_rawconstr f = function
| RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
| RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
| RCases (loc,rtntypopt,tml,pl) ->
- RCases (loc,option_map f rtntypopt,
+ RCases (loc,Option.map f rtntypopt,
List.map (fun (tm,x) -> (f tm,x)) tml,
List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
| RLetTuple (loc,nal,(na,po),b,c) ->
- RLetTuple (loc,nal,(na,option_map f po),f b,f c)
+ RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
| RIf (loc,c,(na,po),b1,b2) ->
- RIf (loc,f c,(na,option_map f po),f b1,f b2)
+ RIf (loc,f c,(na,Option.map f po),f b1,f b2)
| RRec (loc,fk,idl,bl,tyl,bv) ->
RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
Array.map f tyl,Array.map f bv)
@@ -149,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
let g' id e = snd (g id e) in
let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
RCases
- (loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl)
+ (loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl)
| RRec (_,fk,idl,tyl,bv) ->
let idl',e' = fold_ident g idl e in
RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 8ca06e9a5f..4b93388d6e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -40,15 +40,13 @@ type struc_typ = {
let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
let projection_table = ref Cmap.empty
-let option_fold_right f p e = match p with Some a -> f a e | None -> e
-
let load_structure i (_,(ind,id,kl,projs)) =
let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
let struc =
{ s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
structure_table := Indmap.add ind struc !structure_table;
projection_table :=
- List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc))
+ List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
projs !projection_table
let cache_structure o =
@@ -60,7 +58,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
list_smartmap
- (option_smartmap (fun kn -> fst (subst_con subst kn)))
+ (Option.smartmap (fun kn -> fst (subst_con subst kn)))
projs
in
if projs' == projs && kn' == kn then obj else
@@ -68,7 +66,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
let discharge_structure (_,(ind,id,kl,projs)) =
Some (Lib.discharge_inductive ind, id, kl,
- List.map (option_map Lib.discharge_con) projs)
+ List.map (Option.map Lib.discharge_con) projs)
let (inStruc,outStruc) =
declare_object {(default_object "STRUCTURE") with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bb89756b30..c4c9894cb4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -80,7 +80,7 @@ let reference_opt_value sigma env = function
v
| EvalRel n ->
let (_,v,_) = lookup_rel n env in
- option_map (lift n) v
+ Option.map (lift n) v
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-06 11:07:00 +0000