diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 12 |
4 files changed, 11 insertions, 9 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 06058dfe4..956e777b2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -104,7 +104,7 @@ struct type t = cl_index * cl_index let compare (i1, j1) (i2, j2) = let c = Int.compare i1 i2 in - if c = 0 then Int.compare j1 j2 else c + if Int.equal c 0 then Int.compare j1 j2 else c end module ClPairMap = Map.Make(ClPairOrd) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ded8314dd..b4388ff08 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -640,7 +640,7 @@ let apply_on_subterm evdref f c t = match kind_of_term t with | Evar (evk,args) when Evd.is_undefined !evdref evk -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g (_,b,_) a = if b = None then applyrec kc a else a in + let g (_,b,_) a = if Option.is_empty b then applyrec kc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) @@ -653,7 +653,7 @@ let filter_possible_projections c ty ctxt args = let fv2 = collect_vars c in let tyvars = collect_vars ty in List.map2 (fun (id,b,_) a -> - b <> None || + not (Option.is_empty b) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index df0187f73..c8122c4dc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -788,7 +788,7 @@ let closure_of_filter evd evk = function | Some filter -> let evi = Evd.find_undefined evd evk in let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in - let test (id,c,_) b = b || Idset.mem id vars || c <> None in + let test (id,c,_) b = b || Idset.mem id vars || not (Option.is_empty c) in let newfilter = List.map2 test (evar_context evi) filter in if eq_filter newfilter (evar_filter evi) then None else Some newfilter diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 76587a340..8269674d7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -24,8 +24,9 @@ let crazy_type = mkSet let decompose_prod env t = let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in - if name = Anonymous then (Name (Id.of_string "x"),dom,codom) - else res + match name with + | Anonymous -> (Name (Id.of_string "x"), dom, codom) + | Name _ -> res exception Find_at of int @@ -36,7 +37,8 @@ let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do let tagj,arity = reloc_tbl.(j) in - if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then + let no_arity = Int.equal arity 0 in + if Int.equal tag tagj && (cst && no_arity || not (cst || no_arity)) then raise (Find_at j) else () done;raise Not_found @@ -57,7 +59,7 @@ let type_constructor mind mib typ params = let s = ind_subst mind mib in let ctyp = substl s typ in let nparams = Array.length params in - if nparams = 0 then ctyp + if Int.equal nparams 0 then ctyp else let _,ctyp = decompose_prod_n nparams ctyp in substl (Array.rev_to_list params) ctyp @@ -218,7 +220,7 @@ and nf_predicate env ind mip params v pT = let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in - let params = if n=0 then params else Array.map (lift n) params in + let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkInd ind,Array.append params rargs) in let body = nf_vtype (push_rel (name,None,dom) env) vb in true, mkLambda(name,dom,body) |