aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/declarations.ml13
-rw-r--r--checker/term.ml58
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--kernel/nativecode.ml38
-rw-r--r--kernel/nativeconv.ml32
-rw-r--r--kernel/nativelambda.ml27
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/univ.ml2
-rw-r--r--lib/envars.ml18
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/nativenorm.ml23
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--printing/ppconstr.ml26
-rw-r--r--printing/pptactic.ml24
-rw-r--r--printing/ppvernac.ml45
-rw-r--r--printing/prettyp.ml38
-rw-r--r--printing/printer.ml20
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/metasyntax.ml5
-rw-r--r--toplevel/mltop.ml4
21 files changed, 210 insertions, 183 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2ff570a4a..503460422 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -41,6 +41,7 @@ type delta_hint =
module Deltamap = struct
type t = module_path MPmap.t * delta_hint KNmap.t
let empty = MPmap.empty, KNmap.empty
+ let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
let remove_mp mp (mm,km) = (MPmap.remove mp mm, km)
@@ -347,7 +348,7 @@ let from_val a = ref (LSval a)
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
- | _ when mp = mpfrom -> mpto
+ | _ when ModPath.equal mp mpfrom -> mpto
| MPdot (mp1,l) ->
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
if mp1==mp1' then mp
@@ -356,7 +357,7 @@ let rec replace_mp_in_mp mpfrom mpto mp =
let rec mp_in_mp mp mp1 =
match mp1 with
- | _ when mp1 = mp -> true
+ | _ when ModPath.equal mp1 mp -> true
| MPdot (mp2,l) -> mp_in_mp mp mp2
| _ -> false
@@ -429,14 +430,14 @@ let update_delta_resolver resolver1 resolver2 =
let add_delta_resolver resolver1 resolver2 =
if resolver1 == resolver2 then
resolver2
- else if resolver2 = empty_delta_resolver then
+ else if Deltamap.is_empty resolver2 then
resolver1
else
Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
let substition_prefixed_by k mp subst =
let mp_prefixmp kmp (mp_to,reso) sub =
- if mp_in_mp mp kmp && mp <> kmp then
+ if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then
let new_key = replace_mp_in_mp mp k kmp in
Umap.add_mp new_key (mp_to,reso) sub
else sub
@@ -722,7 +723,7 @@ let subst_arity sub = function
(* NB: we leave bytecode and native code fields untouched *)
let subst_const_body sub cb =
{ cb with
- const_hyps = (assert (cb.const_hyps=[]); []);
+ const_hyps = (assert (List.is_empty cb.const_hyps); []);
const_body = subst_constant_def sub cb.const_body;
const_type = subst_arity sub cb.const_type }
@@ -755,7 +756,7 @@ let subst_mind sub mib =
{ mind_record = mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
- mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+ mind_hyps = (assert (List.is_empty mib.mind_hyps); []) ;
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
diff --git a/checker/term.ml b/checker/term.ml
index 8e968904b..bdbc7f8ec 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -197,7 +197,7 @@ let closed0 = closedn 0
let noccurn n term =
let rec occur_rec n c = match c with
- | Rel m -> if m = n then raise LocalOccur
+ | Rel m -> if Int.equal m n then raise LocalOccur
| _ -> iter_constr_with_binders succ occur_rec n c
in
try occur_rec n term; true with LocalOccur -> false
@@ -221,7 +221,7 @@ let noccur_between n m term =
let noccur_with_meta n m term =
let rec occur_rec n c = match c with
- | Rel p -> if n<=p & p<n+m then raise LocalOccur
+ | Rel p -> if n<=p && p<n+m then raise LocalOccur
| App(f,cl) ->
(match f with
| (Cast (Meta _,_,_)| Meta _) -> ()
@@ -291,7 +291,7 @@ let make_substituend c = { sinfo=Unknown; sit=c }
let substn_many lamv n c =
let lv = Array.length lamv in
- if lv = 0 then c
+ if Int.equal lv 0 then c
else
let rec substrec depth c = match c with
| Rel k ->
@@ -383,7 +383,7 @@ let decompose_lam_n_assum n =
if n < 0 then
error "decompose_lam_n_assum: integer parameter must be positive";
let rec lamdec_rec l n c =
- if n=0 then l,c
+ if Int.equal n 0 then l,c
else match c with
| Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
@@ -416,7 +416,7 @@ let decompose_prod_n_assum n =
if n < 0 then
error "decompose_prod_n_assum: integer parameter must be positive";
let rec prodec_rec l n c =
- if n=0 then l,c
+ if Int.equal n 0 then l,c
else match c with
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
@@ -459,40 +459,52 @@ let rec isArity c =
(* alpha conversion : ignore print names and casts *)
+let compare_sorts s1 s2 = match s1, s2 with
+| Prop c1, Prop c2 ->
+ begin match c1, c2 with
+ | Pos, Pos | Null, Null -> true
+ | Pos, Null -> false
+ | Null, Pos -> false
+ end
+| Type u1, Type u2 -> Universe.equal u1 u2
+| Prop _, Type _ -> false
+| Type _, Prop _ -> false
+
let compare_constr f t1 t2 =
match t1, t2 with
- | Rel n1, Rel n2 -> n1 = n2
- | Meta m1, Meta m2 -> m1 = m2
- | Var id1, Var id2 -> id1 = id2
- | Sort s1, Sort s2 -> s1 = s2
+ | Rel n1, Rel n2 -> Int.equal n1 n2
+ | Meta m1, Meta m2 -> Int.equal m1 m2
+ | Var id1, Var id2 -> Id.equal id1 id2
+ | Sort s1, Sort s2 -> compare_sorts s1 s2
| Cast (c1,_,_), _ -> f c1 t2
| _, Cast (c2,_,_) -> f t1 c2
- | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
- | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
- | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+ | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
+ | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
+ | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
| App (c1,l1), App (c2,l2) ->
- if Array.length l1 = Array.length l2 then
- f c1 c2 & Array.for_all2 f l1 l2
+ if Int.equal (Array.length l1) (Array.length l2) then
+ f c1 c2 && Array.for_all2 f l1 l2
else
let (h1,l1) = decompose_app t1 in
let (h2,l2) = decompose_app t2 in
- if List.length l1 = List.length l2 then
- f h1 h2 & List.for_all2 f l1 l2
+ if Int.equal (List.length l1) (List.length l2) then
+ f h1 h2 && List.for_all2 f l1 l2
else false
- | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
| Const c1, Const c2 -> eq_con_chk c1 c2
| Ind c1, Ind c2 -> eq_ind_chk c1 c2
- | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
+ | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
- f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2
- | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
- ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+ f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
+ | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+ Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 &&
+ Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
- ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+ Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| _ -> false
let rec eq_constr m n =
- (m==n) or
+ (m == n) ||
compare_constr eq_constr m n
let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 4d9904694..7aacfa24e 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -123,7 +123,7 @@ let possibly_empty_subentries loc (prods,act) =
| Some id ->
let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in
let rec aux = function
- | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >>
+ | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
| GramNonTerminal(_,OptArgType _,_,p) :: tl ->
bind_name p <:expr< None >> (aux tl)
| GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 41cd830b5..e3e957d95 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -34,7 +34,7 @@ let rec make_when loc = function
let l = make_when loc l in
let loc = CompatLoc.merge loc' loc in
let t = mlexpr_of_argtype loc' t in
- <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
+ <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
| _::l -> make_when loc l
let rec make_let e = function
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 932b490e3..5bdb339d2 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -292,14 +292,14 @@ let fv_lam l =
let mkMLlam params body =
- if Array.length params = 0 then body
+ if Array.is_empty params then body
else
match body with
| MLlam (params', body) -> MLlam(Array.append params params', body)
| _ -> MLlam(params,body)
let mkMLapp f args =
- if Array.length args = 0 then f
+ if Array.is_empty args then f
else
match f with
| MLapp(f,args') -> MLapp(f,Array.append args' args)
@@ -404,18 +404,18 @@ let get_lname (_,l) =
let fv_params env =
let fvn, fvr = !(env.env_named), !(env.env_urel) in
let size = List.length fvn + List.length fvr in
- if size = 0 then empty_params
+ if Int.equal size 0 then empty_params
else begin
let params = Array.make size dummy_lname in
let fvn = ref fvn in
let i = ref 0 in
- while !fvn <> [] do
+ while not (List.is_empty !fvn) do
params.(!i) <- get_lname (List.hd !fvn);
fvn := List.tl !fvn;
incr i
done;
let fvr = ref fvr in
- while !fvr <> [] do
+ while not (List.is_empty !fvr) do
params.(!i) <- get_lname (List.hd !fvr);
fvr := List.tl !fvr;
incr i
@@ -430,19 +430,19 @@ let empty_args = [||]
let fv_args env fvn fvr =
let size = List.length fvn + List.length fvr in
- if size = 0 then empty_args
+ if Int.equal size 0 then empty_args
else
begin
let args = Array.make size (MLint (false,0)) in
let fvn = ref fvn in
let i = ref 0 in
- while !fvn <> [] do
+ while not (List.is_empty !fvn) do
args.(!i) <- get_var env (fst (List.hd !fvn));
fvn := List.tl !fvn;
incr i
done;
let fvr = ref fvr in
- while !fvr <> [] do
+ while not (List.is_empty !fvr) do
let (k,_ as kml) = List.hd !fvr in
let n = get_lname kml in
args.(!i) <- get_rel env n.lname k;
@@ -486,7 +486,7 @@ let rec insert cargs body rl =
let params = rm_params fv params in
rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
| Rcons(l,fv,body',rl) ->
- if body = body' then
+ if Pervasives.(=) body body' then (** FIXME *)
let (c,params) = cargs in
let params = rm_params fv params in
l := (c,params)::!l
@@ -761,7 +761,7 @@ let mllambda_of_lambda auxdefs l t =
| _ -> assert false in
let params =
List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in
- if params = [] then
+ if List.is_empty params then
(!global_stack, ([],[]), ml)
(* final result : global list, fv, ml *)
else
@@ -803,12 +803,12 @@ let subst s l =
let add_subst id v s =
match v with
- | MLlocal id' when id.luid = id'.luid -> s
+ | MLlocal id' when Int.equal id.luid id'.luid -> s
| _ -> LNmap.add id v s
let subst_norm params args s =
let len = Array.length params in
- assert (Array.length args = len && Array.for_all can_subst args);
+ assert (Int.equal (Array.length args) len && Array.for_all can_subst args);
let s = ref s in
for i = 0 to len - 1 do
s := add_subst params.(i) args.(i) !s
@@ -818,7 +818,7 @@ let subst_norm params args s =
let subst_case params args s =
let len = Array.length params in
assert (len > 0 &&
- Array.length args = len &&
+ Int.equal (Array.length args) len &&
let r = ref true and i = ref 0 in
(* we test all arguments excepted the last *)
while !i < len - 1 && !r do r := can_subst args.(!i); incr i done;
@@ -836,7 +836,7 @@ let get_case (_, gcase) i = Int.Map.find i gcase
let all_lam n bs =
let f (_, l) =
match l with
- | MLlam(params, _) -> Array.length params = n
+ | MLlam(params, _) -> Int.equal (Array.length params) n
| _ -> false in
Array.for_all f bs
@@ -894,7 +894,7 @@ let optimize gdef l =
let b2 = optimize s b2 in
begin match t, b2 with
| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
- when l1 = l2 -> MLmatch(annot, l1, b1, bs)
+ when Pervasives.(=) l1 l2 -> MLmatch(annot, l1, b1, bs) (** FIXME *)
| _, _ -> MLif(t, b1, b2)
end
| MLmatch(annot,a,accu,bs) ->
@@ -1190,8 +1190,8 @@ let pp_mllam fmt l =
| Ceq o -> pp_vprim o "eq"
| Clt o -> pp_vprim o "lt"
| Cle o -> pp_vprim o "le"
- | Clt_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b"
- | Cle_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b"
+ | Clt_b -> if Int.equal (Sys.word_size) 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b"
+ | Cle_b -> if Int.equal (Sys.word_size) 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b"
| Ccompare o -> pp_vprim o "compare"
| Cprint o -> pp_vprim o "print"
| Carraymake o -> pp_vprim o "arraymake"
@@ -1243,7 +1243,7 @@ let pp_global fmt g =
| Gtype ((mind, i), lar) ->
let l = string_of_mind mind in
let rec aux s ar =
- if ar = 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
+ if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
let pp_const_sig i fmt j ar =
let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
Format.fprintf fmt " | Construct_%s_%i_%i %s@\n" l i j sig_str
@@ -1267,7 +1267,7 @@ let pp_global fmt g =
(** Compilation of elements in environment {{{**)
let rec compile_with_fv env auxdefs l t =
let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
- if fv_named = [] && fv_rel = [] then (auxdefs,ml)
+ if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
else apply_fv env (fv_named,fv_rel) auxdefs ml
and apply_fv env (fv_named,fv_rel) auxdefs ml =
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 1c931ab85..14b55e91a 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -30,13 +30,14 @@ let rec conv_val pb lvl v1 v2 cu =
let v = mk_rel_accu lvl in
conv_val CONV (lvl+1) (f1 v) (f2 v) cu
| Vconst i1, Vconst i2 ->
- if i1 = i2 then cu else raise NotConvertible
+ if Int.equal i1 i2 then cu else raise NotConvertible
| Vblock b1, Vblock b2 ->
let n1 = block_size b1 in
- if block_tag b1 <> block_tag b2 || n1 <> block_size b2 then
+ let n2 = block_size b2 in
+ if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
raise NotConvertible;
let rec aux lvl max b1 b2 i cu =
- if i = max then
+ if Int.equal i max then
conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu
else
let cu =
@@ -51,8 +52,9 @@ let rec conv_val pb lvl v1 v2 cu =
and conv_accu pb lvl k1 k2 cu =
let n1 = accu_nargs k1 in
- if n1 <> accu_nargs k2 then raise NotConvertible;
- if n1 = 0 then
+ let n2 = accu_nargs k2 in
+ if not (Int.equal n1 n2) then raise NotConvertible;
+ if Int.equal n1 0 then
conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
else
let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
@@ -63,7 +65,7 @@ and conv_atom pb lvl a1 a2 cu =
else
match a1, a2 with
| Arel i1, Arel i2 ->
- if i1 <> i2 then raise NotConvertible;
+ if not (Int.equal i1 i2) then raise NotConvertible;
cu
| Aind ind1, Aind ind2 ->
if not (eq_ind ind1 ind2) then raise NotConvertible;
@@ -74,36 +76,36 @@ and conv_atom pb lvl a1 a2 cu =
| Asort s1, Asort s2 ->
sort_cmp pb s1 s2 cu
| Avar id1, Avar id2 ->
- if id1 <> id2 then raise NotConvertible;
+ if not (Id.equal id1 id2) then raise NotConvertible;
cu
| Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
- if a1.asw_ind <> a2.asw_ind then raise NotConvertible;
+ if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
let cu = conv_accu CONV lvl ac1 ac2 cu in
let tbl = a1.asw_reloc in
let len = Array.length tbl in
- if len = 0 then conv_val CONV lvl p1 p2 cu
+ if Int.equal len 0 then conv_val CONV lvl p1 p2 cu
else
let cu = conv_val CONV lvl p1 p2 cu in
let max = len - 1 in
let rec aux i cu =
let tag,arity = tbl.(i) in
let ci =
- if arity = 0 then mk_const tag
+ if Int.equal arity 0 then mk_const tag
else mk_block tag (mk_rels_accu lvl arity) in
let bi1 = bs1 ci and bi2 = bs2 ci in
- if i = max then conv_val CONV (lvl + arity) bi1 bi2 cu
+ if Int.equal i max then conv_val CONV (lvl + arity) bi1 bi2 cu
else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in
aux 0 cu
| Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
- if s1 <> s2 || rp1 <> rp2 then raise NotConvertible;
+ if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
if f1 == f2 then cu
else conv_fix lvl t1 f1 t2 f2 cu
| (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
(Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
- if s1 <> s2 then raise NotConvertible;
+ if not (Int.equal s1 s2) then raise NotConvertible;
if f1 == f2 then cu
else
- if Array.length f1 <> Array.length f2 then raise NotConvertible
+ if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
else conv_fix lvl t1 f1 t2 f2 cu
| Aprod(_,d1,c1), Aprod(_,d2,c2) ->
let cu = conv_val CONV lvl d1 d2 cu in
@@ -121,7 +123,7 @@ and conv_fix lvl t1 f1 t2 f2 cu =
let cu = conv_val CONV lvl t1.(i) t2.(i) cu in
let fi1 = napply f1.(i) fargs in
let fi2 = napply f2.(i) fargs in
- if i = max then conv_val CONV flvl fi1 fi2 cu
+ if Int.equal i max then conv_val CONV flvl fi1 fi2 cu
else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
aux 0 cu
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 9c400e4c0..b8580f2b3 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -48,14 +48,14 @@ and fix_decl = name array * lambda array * lambda array
(*s Constructors *)
let mkLapp f args =
- if Array.length args = 0 then f
+ if Array.is_empty args then f
else
match f with
| Lapp(f', args') -> Lapp (f', Array.append args' args)
| _ -> Lapp(f, args)
let mkLlam ids body =
- if Array.length ids = 0 then body
+ if Array.is_empty ids then body
else
match body with
| Llam(ids', body) -> Llam(Array.append ids ids', body)
@@ -134,8 +134,7 @@ let map_lam_with_binders g f n lam =
let on_b b =
let (cn,ids,body) = b in
let body' =
- let len = Array.length ids in
- if len = 0 then f n body
+ if Array.is_empty ids then f n body
else f (g (Array.length ids) n) body in
if body == body' then b else (cn,ids,body') in
let br' = Array.smartmap on_b br in
@@ -172,7 +171,7 @@ let rec lam_exlift el lam =
| _ -> map_lam_with_binders el_liftn lam_exlift el lam
let lam_lift k lam =
- if k = 0 then lam
+ if Int.equal k 0 then lam
else lam_exlift (el_shft k el_id) lam
let lam_subst_rel lam id n subst =
@@ -226,7 +225,7 @@ let merge_if t bt bf =
let nt = Array.length idst in
let nf = Array.length idsf in
let common,idst,idsf =
- if nt = nf then idst, [||], [||]
+ if Int.equal nt nf then idst, [||], [||]
else
if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
else idsf, Array.sub idst nf (nt - nf), [||] in
@@ -315,7 +314,7 @@ and reduce_lapp substf lids body substa largs =
let rec occurence k kind lam =
match lam with
| Lrel (_,n) ->
- if n = k then
+ if Int.equal n k then
if kind then false else raise Not_found
else kind
| Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _
@@ -379,13 +378,13 @@ let rec remove_let subst lam =
let is_value lc =
match lc with
| Lval _ -> true
- | Lmakeblock(_,_,_,args) when Array.length args = 0 -> true
+ | Lmakeblock(_,_,_,args) when Array.is_empty args -> true
| _ -> false
let get_value lc =
match lc with
| Lval v -> v
- | Lmakeblock(_,_,tag,args) when Array.length args = 0 ->
+ | Lmakeblock(_,_,tag,args) when Array.is_empty args ->
Nativevalues.mk_int tag
| _ -> raise Not_found
@@ -436,7 +435,7 @@ module Vect =
let length v = v.size
let extend v =
- if v.size = Array.length v.elems then
+ if Int.equal v.size (Array.length v.elems) then
let new_size = min (2*v.size) Sys.max_array_length in
if new_size <= v.size then raise (Invalid_argument "Vect.extend");
let new_elems = Array.make new_size v.elems.(0) in
@@ -470,7 +469,7 @@ module Vect =
let last v =
- if v.size = 0 then raise
+ if Int.equal v.size 0 then raise
(Invalid_argument "Vect.last:index out of bounds");
v.elems.(v.size - 1)
@@ -598,10 +597,10 @@ let rec lambda_of_constr env c =
let cn = (ind,i+1) in
let _, arity = tbl.(i) in
let b = lambda_of_constr env b in
- if arity = 0 then (cn, empty_ids, b)
+ if Int.equal arity 0 then (cn, empty_ids, b)
else
match b with
- | Llam(ids, body) when Array.length ids = arity -> (cn, ids, body)
+ | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body)
| _ ->
let ids = Array.make arity Anonymous in
let args = make_args arity 1 in
@@ -649,7 +648,7 @@ and lambda_of_app env f args =
let tag, nparams, arity = Renv.get_construct_info env c in
let expected = nparams + arity in
let nargs = Array.length args in
- if nargs = expected then
+ if Int.equal nargs expected then
let args = lambda_of_args env nparams args in
makeblock !global_env c tag args
else
diff --git a/kernel/term.ml b/kernel/term.ml
index 14154b6c8..a052d6dfc 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -76,6 +76,8 @@ let sorts_ord s1 s2 =
| Prop _, Type _ -> -1
| Type _, Prop _ -> 1
+let sorts_eq s1 s2 = Int.equal (sorts_ord s1 s2) 0
+
let is_prop_sort = function
| Prop Null -> true
| _ -> false
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f1d44a9a5..f0501358b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -510,7 +510,7 @@ let merge g arcu arcv =
let merge_disc g arc1 arc2 =
let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
let arcu, g =
- if arc1.rank <> arc2.rank then arcu, g
+ if not (Int.equal arc1.rank arc2.rank) then arcu, g
else
let arcu = {arcu with rank = succ arcu.rank} in
arcu, enter_arc arcu g
diff --git a/lib/envars.ml b/lib/envars.ml
index 8e7baa082..47ecdb400 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -33,7 +33,7 @@ let home ~warn =
Filename.current_dir_name))
let path_to_list p =
- let sep = if Sys.os_type = "Win32" then ';' else ':' in
+ let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
String.split sep p
let user_path () =
@@ -53,12 +53,12 @@ let rec which l f =
let expand_path_macros ~warn s =
let rec expand_atom s i =
let l = String.length s in
- if i<l && (Util.is_digit s.[i] or Util.is_letter s.[i] or s.[i] = '_')
+ if i<l && (Util.is_digit s.[i] || Util.is_letter s.[i] || s.[i] == '_')
then expand_atom s (i+1)
else i in
let rec expand_macros s i =
let l = String.length s in
- if i=l then s else
+ if Int.equal i l then s else
match s.[i] with
| '$' ->
let n = expand_atom s (i+1) in
@@ -68,7 +68,7 @@ let expand_path_macros ~warn s =
| '~' when Int.equal i 0 ->
let n = expand_atom s (i+1) in
let v =
- if n=i+1 then home ~warn
+ if Int.equal n (i + 1) then home ~warn
else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir
in
let s = v^(String.sub s n (l-n)) in
@@ -94,7 +94,7 @@ let coqroot =
(** On win32, we add coqbin to the PATH at launch-time (this used to be
done in a .bat script). *)
let _ =
- if Coq_config.arch = "win32" then
+ if String.equal Coq_config.arch "win32" then
Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
(** [reldir instdir testfile oth] checks if [testfile] exists in
@@ -109,7 +109,7 @@ let reldir instdir testfile oth =
let guess_coqlib fail =
let file = "theories/Init/Prelude.vo" in
- reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file
+ reldir (if String.equal Coq_config.arch "win32" then ["lib"] else ["lib";"coq"]) file
(fun () ->
let coqlib = match Coq_config.coqlib with
| Some coqlib -> coqlib
@@ -130,7 +130,7 @@ let coqlib ~fail =
let docdir () =
reldir (
- if Coq_config.arch = "win32" then
+ if String.equal Coq_config.arch "win32" then
["doc"]
else
["share";"doc";"coq"]
@@ -210,7 +210,7 @@ let xdg_data_dirs warn =
try
List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
with
- | Not_found when Sys.os_type = "Win32" -> [relative_base / "share"]
+ | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"]
| Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
in
xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir
@@ -220,7 +220,7 @@ let xdg_config_dirs warn =
try
List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
with
- | Not_found when Sys.os_type = "Win32" -> [relative_base / "config"]
+ | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "config"]
| Not_found -> ["/etc/xdg/coq"]
in
xdg_config_home warn :: sys_dirs @ opt2list Coq_config.configdir
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 497c3b9df..7c63c970d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -294,9 +294,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ev apprF apprM i
and f2 i =
match switch (ise_stack2 not_only_app env i (evar_conv_x ts)) skF skM with
- |Some (l,r), Success i' when on_left && (not_only_app || l = []) ->
+ |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
- |Some (r,l), Success i' when not on_left && (not_only_app || l = []) ->
+ |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
|None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termM
|_, (UnifFailure _ as x) -> x
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 6af9ff323..f65ccc5ba 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -29,7 +29,7 @@ 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
+ if Int.equal tag tagj && (cst && Int.equal arity 0 || not(cst || Int.equal arity 0)) then
raise (Find_at j)
else ()
done;raise Not_found
@@ -37,8 +37,9 @@ let invert_tag cst tag reloc_tbl =
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)
+ | _ -> res
let app_type env c =
let t = whd_betadeltaiota env c in
@@ -57,7 +58,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 (List.rev (Array.to_list params)) ctyp
@@ -135,12 +136,14 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- if engagement env = Some ImpredicativeSet then
+ begin match engagement env with
+ | Some ImpredicativeSet ->
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- else
+ | _ ->
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (sup u1 type0_univ)
+ end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (sup type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
@@ -155,7 +158,7 @@ let branch_of_switch lvl ans bs =
let branch i =
let tag,arity = tbl.(i) in
let ci =
- if arity = 0 then mk_const tag
+ if Int.equal arity 0 then mk_const tag
else mk_block tag (mk_rels_accu lvl arity) in
bs ci in
Array.init (Array.length tbl) branch
@@ -195,7 +198,7 @@ and nf_type_sort env v =
and nf_accu env accu =
let atom = atom_of_accu accu in
- if accu_nargs accu = 0 then nf_atom env atom
+ if Int.equal (accu_nargs accu) 0 then nf_atom env atom
else
let a,typ = nf_atom_type env atom in
let _, args = nf_args env accu typ in
@@ -203,7 +206,7 @@ and nf_accu env accu =
and nf_accu_type env accu =
let atom = atom_of_accu accu in
- if accu_nargs accu = 0 then nf_atom_type env atom
+ if Int.equal (accu_nargs accu) 0 then nf_atom_type env atom
else
let a,typ = nf_atom_type env atom in
let t, args = nf_args env accu typ in
@@ -320,7 +323,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_type (push_rel (name,None,dom) env) vb in
true, mkLambda(name,dom,body)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7b1a514ed..72de7f471 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -285,7 +285,7 @@ let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst =
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
- if bodynum = ind && not (Option.is_empty cst) then
+ if Int.equal bodynum ind && not (Option.is_empty cst) then
let (c,params) = Option.get cst in
applist(c, List.rev params)
else
@@ -314,7 +314,7 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies))
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
- if bodynum = ind && not (Option.is_empty cst) then
+ if Int.equal bodynum ind && not (Option.is_empty cst) then
let (c,params) = Option.get cst in
applist(c, List.rev params)
else
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4c0771aef..a389ee175 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -46,7 +46,7 @@ let lsimpleconstr = (8,E)
let lsimplepatt = (1,E)
let prec_less child (parent,assoc) =
- if parent < 0 && child = lprod then true
+ if parent < 0 && Int.equal child lprod then true
else
let parent = abs parent in
match assoc with
@@ -100,7 +100,7 @@ let pr_generalization bk ak c =
str "`" ++ str hd ++ c ++ str tl
let pr_com_at n =
- if Flags.do_beautify() && n <> 0 then comment n
+ if Flags.do_beautify() && not (Int.equal n 0) then comment n
else mt()
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
@@ -136,7 +136,7 @@ let pr_opt_type_spc pr = function
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
let pr_lident (loc,id) =
- if loc <> Loc.ghost then
+ if not (Loc.is_ghost loc) then
let (b,_) = Loc.unloc loc in
pr_located pr_id (Loc.make_loc (b,b+String.length(Id.to_string id)),id)
else pr_id id
@@ -191,8 +191,8 @@ let rec pr_patt sep inh p =
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
| CPatNotation (_,s,(l,ll),args) ->
let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in
- (if args=[]||prec_less l_not (lapp,L) then strm_not else surround strm_not)
- ++ prlist (pr_patt spc (lapp,L)) args, if args<>[] then lapp else l_not
+ (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
+ ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
| CPatPrim (_,p) -> pr_prim_token p, latom
| CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1
in
@@ -233,7 +233,7 @@ let surround_implicit k p =
let pr_binder many pr (nal,k,t) =
match k with
| Generalized (b, b', t') ->
- assert (b=Implicit);
+ assert (match b with Implicit -> true | _ -> false);
begin match nal with
|[loc,Anonymous] ->
hov 1 (str"`" ++ (surround_impl b'
@@ -447,7 +447,7 @@ let pr pr sep inherited a =
pr_fun_sep ++ pr spc ltop a),
llambda
| CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
- when x=x' ->
+ when Id.equal x x' ->
hv 0 (
hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++
pr spc ltop b),
@@ -462,21 +462,21 @@ let pr pr sep inherited a =
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
let p = pr_proj (pr mt) pr_appexpl c f l1 in
- if l2<>[] then
+ if not (List.is_empty l2) then
p ++ prlist (pr spc (lapp,L)) l2, lapp
else
p, lproj
| CAppExpl (_,(None,Ident (_,var)),[t])
| CApp (_,(_,CRef(Ident(_,var))),[t,None])
- when var = Notation_ops.ldots_var ->
+ when Id.equal var Notation_ops.ldots_var ->
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
| CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
| CApp (_,(Some i,f),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
- assert (snd c = None);
+ assert (Option.is_empty (snd c));
let p = pr_proj (pr mt) pr_app (fst c) f l1 in
- if l2<>[] then
+ if not (List.is_empty l2) then
p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
else
p, lproj
@@ -605,7 +605,7 @@ let pr_red_flag pr r =
(if r.rBeta then pr_arg str "beta" else mt ()) ++
(if r.rIota then pr_arg str "iota" else mt ()) ++
(if r.rZeta then pr_arg str "zeta" else mt ()) ++
- (if r.rConst = [] then
+ (if List.is_empty r.rConst then
if r.rDelta then pr_arg str "delta"
else mt ()
else
@@ -619,7 +619,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| Hnf -> str "hnf"
| Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o
| Cbv f ->
- if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
+ if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
str "compute"
else
hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 14fae2612..5a2ed5bc5 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -423,17 +423,20 @@ let pr_in_hyp_as pr_id = function
let pr_clauses default_is_concl pr_id = function
| { onhyps=Some []; concl_occs=AllOccurrences }
- when default_is_concl = Some true -> mt ()
+ when (match default_is_concl with Some true -> true | _ -> false) -> mt ()
| { onhyps=None; concl_occs=AllOccurrences }
- when default_is_concl = Some false -> mt ()
+ when (match default_is_concl with Some false -> true | _ -> false) -> mt ()
+ | { onhyps=None; concl_occs=NoOccurrences } ->
+ pr_in (str " * |-")
| { onhyps=None; concl_occs=occs } ->
- if occs = NoOccurrences then pr_in (str " * |-")
- else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
+ pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
| { onhyps=Some l; concl_occs=occs } ->
+ let pr_occs = match occs with
+ | NoOccurrences -> mt ()
+ | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
+ in
pr_in
- (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++
- (if occs = NoOccurrences then mt ()
- else pr_with_occurrences (fun () -> str" |- *") (occs,())))
+ (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
let pr_orient b = if b then mt () else str "<- "
@@ -483,7 +486,7 @@ let pr_match_rule m pr pr_pat = function
| Pat (rl,mp,t) ->
hov 0 (
hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
- (if rl <> [] then spc () else mt ()) ++
+ (if not (List.is_empty rl) then spc () else mt ()) ++
hov 0 (
str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
str "=>" ++ brk (1,4) ++ pr t))
@@ -706,7 +709,7 @@ and pr_atom1 = function
| TacGeneralizeDep c ->
hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
pr_constrarg c)
- | TacLetTac (na,c,cl,true,_) when cl = Locusops.nowhere ->
+ | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
| TacLetTac (na,c,cl,b,e) ->
hov 1 ((if b then str "set" else str "remember") ++
@@ -921,7 +924,8 @@ let rec pr_tac inherited tac =
pr_tac (lorelse,E) t2),
lorelse
| TacFail (n,l) ->
- hov 1 (str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++
+ let arg = match n with ArgArg 0 -> mt () | _ -> pr_arg (pr_or_var int) n in
+ hov 1 (str "fail" ++ arg ++
prlist (pr_arg (pr_message_token pr_ident)) l), latom
| TacFirst tl ->
str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 0082993b7..d2f5beedf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -26,7 +26,7 @@ open Declaremods
let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
let pr_lident (loc,id) =
- if loc <> Loc.ghost then
+ if Loc.is_ghost loc then
let (b,_) = Loc.unloc loc in
pr_located pr_id (Loc.make_loc (b,b+String.length(Id.to_string id)),id)
else pr_id id
@@ -37,7 +37,7 @@ let string_of_fqid fqid =
let pr_fqid fqid = str (string_of_fqid fqid)
let pr_lfqid (loc,fqid) =
- if loc <> Loc.ghost then
+ if Loc.is_ghost loc then
let (b,_) = Loc.unloc loc in
pr_located pr_fqid (Loc.make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
else
@@ -82,7 +82,7 @@ let rec extract_signature = function
let rec match_vernac_rule tys = function
[] -> raise Not_found
| pargs::rls ->
- if extract_signature pargs = tys then pargs
+ if List.equal Genarg.argument_type_eq (extract_signature pargs) tys then pargs
else match_vernac_rule tys rls
let sep = fun _ -> spc()
@@ -105,12 +105,12 @@ let pr_set_entry_type = function
let strip_meta id =
let s = Id.to_string id in
- if s.[0]='$' then Id.of_string (String.sub s 1 (String.length s - 1))
+ if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1))
else id
let pr_production_item = function
| TacNonTerm (loc,nt,Some (p,sep)) ->
- let pp_sep = if sep <> "" then str "," ++ quote (str sep) else mt () in
+ let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
| TacNonTerm (loc,nt,None) -> str nt
| TacTerm s -> qs s
@@ -229,8 +229,8 @@ let rec pr_module_ast pr_c = function
hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
- let sep () = if scl=[] then mt () else str "," in
- if ann = DefaultInline && scl = [] then mt ()
+ let sep () = if List.is_empty scl then mt () else str "," in
+ if ann == DefaultInline && List.is_empty scl then mt ()
else
str " [" ++
(match ann with
@@ -347,8 +347,11 @@ let rec factorize = function
| [] -> []
| (c,(idl,t))::l ->
match factorize l with
- | (xl,t')::l' when t' = (c,t) -> (idl@xl,t')::l'
- | l' -> (idl,(c,t))::l'
+ | (xl,((c', t') as r))::l'
+ when (c : bool) == c' && Pervasives.(=) t t' ->
+ (** FIXME: we need equality on constr_expr *)
+ (idl@xl,r)::l'
+ | l' -> (idl,(c,t))::l'
let pr_ne_params_list pr_c l =
match factorize l with
@@ -384,7 +387,7 @@ let pr_syntax_modifiers = function
hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
let print_level n =
- if n <> 0 then str " (at level " ++ int n ++ str ")" else mt ()
+ if not (Int.equal n 0) then str " (at level " ++ int n ++ str ")" else mt ()
let pr_grammar_tactic_rule n (_,pil,t) =
hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++
@@ -392,7 +395,7 @@ let pr_grammar_tactic_rule n (_,pil,t) =
spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
let pr_statement head (id,(bl,c,guard)) =
- assert (id<>None);
+ assert (not (Option.is_empty id));
hov 1
(head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
(match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
@@ -570,7 +573,7 @@ let rec pr_vernac = function
| VernacNotation (local,c,((_,s),l),opt) ->
let ps =
let n = String.length s in
- if n > 2 & s.[0] = '\'' & s.[n-1] = '\''
+ if n > 2 && s.[0] == '\'' && s.[n-1] == '\''
then
let s' = String.sub s 1 (n-2) in
if String.contains s' '\'' then qs s else str s'
@@ -746,7 +749,7 @@ let rec pr_vernac = function
hov 2 (str"Module" ++ spc() ++ pr_require_token export ++
pr_lident m ++ b ++
pr_of_module_type pr_lconstr tys ++
- (if bd = [] then mt () else str ":= ") ++
+ (if List.is_empty bd then mt () else str ":= ") ++
prlist_with_sep (fun () -> str " <+ ")
(pr_module_ast_inl pr_lconstr) bd)
| VernacDeclareModule (export,id,bl,m1) ->
@@ -759,7 +762,7 @@ let rec pr_vernac = function
let pr_mt = pr_module_ast_inl pr_lconstr in
hov 2 (str"Module Type " ++ pr_lident id ++ b ++
prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++
- (if m = [] then mt () else str ":= ") ++
+ (if List.is_empty m then mt () else str ":= ") ++
prlist_with_sep (fun () -> str " <+ ") pr_mt m)
| VernacInclude (mexprs) ->
let pr_m = pr_module_ast_inl pr_lconstr in
@@ -767,7 +770,7 @@ let rec pr_vernac = function
prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
(* Solving *)
| VernacSolve (i,tac,deftac) ->
- (if i = 1 then mt() else int i ++ str ": ") ++
+ (if Int.equal i 1 then mt() else int i ++ str ": ") ++
pr_raw_tactic tac
++ (if deftac then str ".." else mt ())
| VernacSolveExistential (i,c) ->
@@ -802,7 +805,7 @@ let rec pr_vernac = function
prlist (function None -> str " _"
| Some id -> spc () ++ pr_id id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
- let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
+ let idl = List.map_filter (fun x -> x) idl in
pr_raw_tactic_env
(idl @ List.map coerce_reference_to_id
(List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
@@ -852,7 +855,7 @@ let rec pr_vernac = function
spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
aux (n-1) tl in
prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
- if mods <> [] then str" : " else str"" ++
+ if not (List.is_empty mods) then str" : " else str"" ++
prlist_with_sep (fun () -> str", " ++ spc()) (function
| `SimplDontExposeCase -> str "simpl nomatch"
| `SimplNeverUnfold -> str "simpl never"
@@ -875,7 +878,7 @@ let rec pr_vernac = function
| Some idl ->
str (if List.length idl > 1 then "s " else " ") ++
prlist_with_sep spc pr_lident idl)
- | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent ->
+ | VernacSetOpacity(b,[k,l]) when Conv_oracle.is_transparent k ->
hov 1 (pr_non_locality b ++ str "Transparent" ++
spc() ++ prlist_with_sep sep pr_smart_global l)
| VernacSetOpacity(b,[Conv_oracle.Opaque,l]) ->
@@ -885,7 +888,7 @@ let rec pr_vernac = function
let pr_lev = function
Conv_oracle.Opaque -> str"opaque"
| Conv_oracle.Expand -> str"expand"
- | l when l = Conv_oracle.transparent -> str"transparent"
+ | l when Conv_oracle.is_transparent l -> str"transparent"
| Conv_oracle.Level n -> int n in
let pr_line (l,q) =
hov 2 (pr_lev l ++ spc() ++
@@ -908,8 +911,8 @@ let rec pr_vernac = function
spc() ++ str"in" ++ spc () ++ pr_lconstr c)
| None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c)
in
- (if io = None then mt() else int (Option.get io) ++ str ": ") ++
- pr_mayeval r c
+ let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in
+ pr_i ++ pr_mayeval r c
| VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
| VernacDeclareReduction (b,s,r) ->
pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 18bfeb6d6..f7f877ddf 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -53,13 +53,13 @@ let print_closed_sections = ref false
let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l)
-let with_line_skip l = if l = [] then mt() else fnl() ++ fnl () ++ pr_infos_list l
+let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l
let blankline = mt() (* add a blank sentence in the list of infos *)
let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": "
-let int_or_no n = if n=0 then str "no" else int n
+let int_or_no n = if Int.equal n 0 then str "no" else int n
(*******************)
(** Basic printing *)
@@ -108,8 +108,8 @@ let print_impargs_list prefix l =
[v 2 (prlist_with_sep cut (fun x -> x)
[(if ismt prefix then str "When" else prefix ++ str ", when") ++
str " applied to " ++
- (if n1 = n2 then int_or_no n2 else
- if n1 = 0 then str "less than " ++ int n2
+ (if Int.equal n1 n2 then int_or_no n2 else
+ if Int.equal n1 0 then str "less than " ++ int n2
else int n1 ++ str " to " ++ int_or_no n2) ++
str (String.plural n2 " argument") ++ str ":";
v 0 (prlist_with_sep cut (fun x -> x)
@@ -118,22 +118,22 @@ let print_impargs_list prefix l =
else [str "No implicit arguments"]))])]) l)
let print_renames_list prefix l =
- if l = [] then [] else
+ if List.is_empty l then [] else
[add_colon prefix ++ str "Arguments are renamed to " ++
hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))]
let need_expansion impl ref =
let typ = Global.type_of_global ref in
- let ctx = (prod_assum typ) in
- let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
- impl <> [] & List.length impl >= nprods &
+ let ctx = prod_assum typ in
+ let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in
+ not (List.is_empty impl) && List.length impl >= nprods &
let _,lastimpl = List.chop nprods impl in
- List.filter is_status_implicit lastimpl <> []
+ List.exists is_status_implicit lastimpl
let print_impargs ref =
let ref = Smartlocate.smart_global ref in
let impl = implicits_of_global ref in
- let has_impl = impl <> [] in
+ let has_impl = not (List.is_empty impl) in
(* Need to reduce since implicits are computed with products flattened *)
pr_infos_list
([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
@@ -147,7 +147,7 @@ let print_impargs ref =
let print_argument_scopes prefix = function
| [Some sc] ->
[add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"]
- | l when not (List.for_all ((=) None) l) ->
+ | l when not (List.for_all Option.is_empty l) ->
[add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++
str "[" ++
pr_sequence (function Some sc -> str sc | None -> str "_") l ++
@@ -196,7 +196,7 @@ type opacity =
| TransparentMaybeOpacified of Conv_oracle.level
let opacity env = function
- | VarRef v when pi2 (Environ.lookup_named v env) <> None ->
+ | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) ->
Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v)))
| ConstRef cst ->
let cb = Environ.lookup_constant cst env in
@@ -216,7 +216,7 @@ let print_opacity ref =
| FullyOpaque -> "opaque"
| TransparentMaybeOpacified Conv_oracle.Opaque ->
"basically transparent but considered opaque for reduction"
- | TransparentMaybeOpacified lev when lev = Conv_oracle.transparent ->
+ | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
"transparent"
| TransparentMaybeOpacified (Conv_oracle.Level n) ->
"transparent (with expansion weight "^string_of_int n^")"
@@ -261,18 +261,18 @@ let print_args_data_of_inductive_ids get test pr sp mipv =
let print_inductive_implicit_args =
print_args_data_of_inductive_ids
- implicits_of_global (fun l -> positions_of_implicits l <> [])
+ implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l)))
print_impargs_list
let print_inductive_renames =
print_args_data_of_inductive_ids
(fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
- ((<>) Anonymous)
+ ((!=) Anonymous)
print_renames_list
let print_inductive_argument_scopes =
print_args_data_of_inductive_ids
- Notation.find_arguments_scope ((<>) None) print_argument_scopes
+ Notation.find_arguments_scope (Option.has_some) print_argument_scopes
(*********************)
(* "Locate" commands *)
@@ -339,7 +339,7 @@ let print_located_qualid ref =
prlist_with_sep fnl
(fun (o,oqid) ->
hov 2 (pr_located_qualid o ++
- (if oqid <> qid then
+ (if not (qualid_eq oqid qid) then
spc() ++ str "(shorter name to refer to it in current context is " ++ pr_qualid oqid ++ str")"
else
mt ()))) l
@@ -483,7 +483,7 @@ let gallina_print_library_entry with_values ent =
let gallina_print_context with_values =
let rec prec n = function
- | h::rest when n = None or Option.get n > 0 ->
+ | h::rest when Option.is_empty n || 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 ())
@@ -606,7 +606,7 @@ let read_sec_context r =
user_err_loc (loc,"read_sec_context", str "Unknown section.") in
let rec get_cxt in_cxt = function
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
- if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
+ if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| (_,Lib.ClosedSection _)::rest ->
error "Cannot print the contents of a closed section."
(* LEM: Actually, we could if we wanted to. *)
diff --git a/printing/printer.ml b/printing/printer.ml
index d0a61bb11..e73ccfb35 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -209,8 +209,8 @@ let pr_context_unlimited env =
(sign_env ++ db_env)
let pr_ne_context_of header env =
- if Environ.rel_context env = empty_rel_context &
- Environ.named_context env = empty_named_context then (mt ())
+ if List.is_empty (Environ.rel_context env) &&
+ List.is_empty (Environ.named_context env) then (mt ())
else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ())
let pr_context_limit n env =
@@ -253,9 +253,9 @@ let pr_predicate pr_elt (b, elts) =
let pr_elts = prlist_with_sep spc pr_elt elts in
if b then
str"all" ++
- (if elts = [] then mt () else str" except: " ++ pr_elts)
+ (if List.is_empty elts then mt () else str" except: " ++ pr_elts)
else
- if elts = [] then str"none" else pr_elts
+ if List.is_empty elts then str"none" else pr_elts
let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p)
@@ -299,7 +299,7 @@ let pr_evgl_sign gl =
let _, l = List.filter2 (fun b c -> not b) (evar_filter gl) (evar_context gl) in
let ids = List.rev_map pi1 l in
let warn =
- if ids = [] then mt () else
+ if List.is_empty ids then mt () else
(str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
let pc = pr_lconstr gl.evar_concl in
@@ -324,7 +324,7 @@ let default_pr_subgoal n sigma =
let rec prrec p = function
| [] -> error "No such goal."
| g::rest ->
- if p = 1 then
+ if Int.equal p 1 then
let pg = default_pr_goal { sigma=sigma ; it=g } in
v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
++ str " is:" ++ cut () ++ pg)
@@ -390,7 +390,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
str ".")
| None ->
let exl = Evarutil.non_instantiated sigma in
- if exl = [] then
+ if List.is_empty exl then
(str"No more subgoals."
++ emacs_print_dependent_evars sigma seeds)
else
@@ -515,7 +515,7 @@ let pr_prim_rule = function
(str"fix " ++ pr_id f ++ str"/" ++ int n)
| FixRule (f,n,others,j) ->
- if j<>0 then msg_warning (strbrk "Unsupported printing of \"fix\"");
+ if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
let rec print_mut = function
| (f,n,ar)::oth ->
pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -527,7 +527,7 @@ let pr_prim_rule = function
(str"cofix " ++ pr_id f)
| Cofix (f,others,j) ->
- if j<>0 then msg_warning (strbrk "Unsupported printing of \"fix\"");
+ if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
let rec print_mut = function
| (f,ar)::oth ->
(pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
@@ -647,7 +647,7 @@ open Termops
open Reduction
let print_params env params =
- if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
+ if List.is_empty params then mt () else pr_rel_context env params ++ brk(1,2)
let print_constructors envpar names types =
let pc =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9680a0046..4c2e06331 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -165,18 +165,18 @@ let explain_unification_error env sigma p1 p2 = function
spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk)
++ strbrk " because " ++ pr_lconstr_env env c ++
strbrk " is not in its scope" ++
- (if args = [||] then mt() else
+ (if Array.is_empty args then mt() else
strbrk ": available arguments are " ++
pr_sequence (pr_lconstr_env env) (List.rev (Array.to_list args))) ++
str ")"
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) mt ()
| ConversionFailed (env,t1,t2) ->
- if eq_constr t1 p1 & eq_constr t2 p2 then mt () else
+ if eq_constr t1 p1 && eq_constr t2 p2 then mt () else
let env = make_all_name_different env in
let t1 = Evarutil.nf_evar sigma t1 in
let t2 = Evarutil.nf_evar sigma t2 in
- if t1 <> p1 || t2 <> p2 then
+ if not (eq_constr t1 p1) || not (eq_constr t2 p2) then
spc () ++ str "(cannot unify " ++ pr_lconstr_env env t1 ++
strbrk " and " ++ pr_lconstr_env env t2 ++ str ")"
else mt ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1e41cdec8..a1b9574d8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -456,8 +456,9 @@ let is_non_terminal = function
| NonTerminal _ | SProdList _ -> true
| _ -> false
-let is_next_non_terminal prods =
- prods <> [] && is_non_terminal (List.hd prods)
+let is_next_non_terminal = function
+| [] -> false
+| pr :: _ -> is_non_terminal pr
let is_next_terminal = function Terminal _ :: _ -> true | _ -> false
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index c4d9dcaf4..e5e4ff599 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -101,10 +101,10 @@ let report_on_load_obj_error exc =
let x = Obj.repr exc in
(* Try an horrible (fragile) hack to report on Symtable dynlink errors *)
(* (we follow ocaml's Printexc.to_string decoding of exceptions) *)
- if Obj.is_block x && Obj.magic(Obj.field (Obj.field x 0) 0) = "Symtable.Error"
+ if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error"
then
let err_block = Obj.field x 1 in
- if Obj.tag err_block = 0 then
+ if Int.equal (Obj.tag err_block) 0 then
(* Symtable.Undefined_global of string *)
str "reference to undefined global " ++
str (Obj.magic (Obj.field err_block 0))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:24:29 +0000