aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--grammar/vernacextend.ml42
-rw-r--r--ide/coqide.ml2
-rw-r--r--ide/coqide_ui.ml2
-rw-r--r--interp/constrexpr_ops.ml7
-rw-r--r--kernel/cbytegen.ml20
-rw-r--r--kernel/closure.ml14
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/environ.ml11
-rw-r--r--kernel/esubst.ml2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/mod_subst.ml14
-rw-r--r--kernel/modops.ml8
-rw-r--r--kernel/names.ml23
-rw-r--r--kernel/names.mli7
-rw-r--r--kernel/pre_env.ml2
-rw-r--r--kernel/reduction.ml36
-rw-r--r--kernel/sign.ml2
-rw-r--r--kernel/term.ml106
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/univ.ml27
-rw-r--r--lib/cArray.ml4
-rw-r--r--lib/rtree.ml19
-rw-r--r--lib/system.ml10
-rw-r--r--lib/util.ml2
-rw-r--r--library/libnames.ml15
-rw-r--r--library/nameops.ml10
-rw-r--r--parsing/g_tactic.ml471
-rw-r--r--parsing/g_xml.ml48
-rw-r--r--parsing/lexer.ml442
-rw-r--r--parsing/pcoq.ml486
-rw-r--r--plugins/firstorder/unify.ml2
32 files changed, 345 insertions, 219 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index cebfaa615..3bbc14038 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -205,7 +205,7 @@ EXTEND
let t, g = interp_entry_name false None e sep in
GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| s = STRING ->
- if s = "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+ if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
GramTerminal s
] ]
;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3550e75e3..321cacbf7 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -84,7 +84,7 @@ EXTEND
rule:
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
->
- if s = "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+ if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
(Some s,l,<:expr< fun () -> $e$ >>)
| "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
(None,l,<:expr< fun () -> $e$ >>)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0fac50abe..4f830a421 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1703,7 +1703,7 @@ let main files =
let windows_actions = GAction.action_group ~name:"Windows" () in
let help_actions = GAction.action_group ~name:"Help" () in
let add_gen_actions menu_name act_grp l =
- let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) in
+ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) in
let add_simple_template menu_name act_grp text =
let text' =
let l = String.length text - 1 in
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 2ec72fc1a..36e071e86 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -1,6 +1,6 @@
let ui_m = GAction.ui_manager ();;
-let no_under = Util.string_map (fun x -> if x = '_' then '-' else x)
+let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
let list_items menu li =
let res_buf = Buffer.create 500 in
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 306fbfad9..6b45c8897 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -73,9 +73,10 @@ let local_binder_loc = function
| LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
| LocalRawAssum ([],_,_) -> assert false
-let local_binders_loc bll =
- if bll = [] then Loc.ghost else
- Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
+let local_binders_loc bll = match bll with
+ | [] -> Loc.ghost
+ | h :: l ->
+ Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index deba56f73..1d2587efe 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -179,16 +179,17 @@ let push_local sz r =
(*i Compilation of variables *)
-let find_at el l =
+let find_at f l =
let rec aux n = function
| [] -> raise Not_found
- | hd :: tl -> if hd = el then n else aux (n+1) tl
+ | hd :: tl -> if f hd then n else aux (n + 1) tl
in aux 1 l
let pos_named id r =
let env = !(r.in_env) in
let cid = FVnamed id in
- try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
+ let f = function FVnamed id' -> id_eq id id' | _ -> false in
+ try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
with Not_found ->
let pos = env.size in
r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev};
@@ -206,7 +207,8 @@ let pos_rel i r sz =
let i = i - r.nb_rec in
let db = FVrel(i) in
let env = !(r.in_env) in
- try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
+ let f = function FVrel j -> Int.equal i j | _ -> false in
+ try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
with Not_found ->
let pos = env.size in
r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
@@ -357,7 +359,7 @@ let rec str_const c =
let oip = oib.mind_packets.(j) in
let num,arity = oip.mind_reloc_tbl.(i-1) in
let nparams = oib.mind_nparams in
- if nparams + arity = Array.length args then
+ if Int.equal (nparams + arity) (Array.length args) then
(* spiwack: *)
(* 1/ tries to compile the constructor in an optimal way,
it is supposed to work only if the arguments are
@@ -609,7 +611,7 @@ let rec compile_constr reloc c sz cont =
let lbl_sw = Label.create () in
let sz_b,branch,is_tailcall =
match branch1 with
- | Kreturn k -> assert (k = sz); sz, branch1, true
+ | Kreturn k -> assert (Int.equal k sz); sz, branch1, true
| _ -> sz+3, Kjump, false
in
let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -632,7 +634,7 @@ let rec compile_constr reloc c sz cont =
let nargs = List.length args in
let lbl_b,code_b =
label_code(
- if nargs = arity then
+ if Int.equal nargs arity then
Kpushfields arity ::
compile_constr (push_param arity sz_b reloc)
body (sz_b+arity) (add_pop arity (branch :: !c))
@@ -844,7 +846,7 @@ let op_compilation n op =
fun kn fc reloc args sz cont ->
if not fc then raise Not_found else
let nargs = Array.length args in
- if nargs=n then (*if it is a fully applied addition*)
+ if Int.equal nargs n then (*if it is a fully applied addition*)
let (escape, labeled_cont) = make_branch cont in
let else_lbl = Label.create () in
comp_args compile_constr reloc args sz
@@ -854,7 +856,7 @@ let op_compilation n op =
(* works as comp_app with nargs = n and non-tailcall cont*)
Kgetglobal (get_allias !global_env kn)::
Kapply n::labeled_cont)))
- else if nargs=0 then
+ else if Int.equal nargs 0 then
code_construct kn cont
else
comp_app (fun _ _ _ cont -> code_construct kn cont)
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 681fb8533..1c9b2145d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -327,7 +327,7 @@ and fterm =
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
+let is_val v = match v.norm with Norm -> true | _ -> false
let mk_atom c = {norm=Norm;term=FAtom c}
@@ -426,9 +426,9 @@ let rec lft_fconstr n ft =
| FLOCKED -> assert false
| _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
- if k=0 then f else lft_fconstr k f
+ if Int.equal k 0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
- if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
+ if Int.equal k 0 then v else Array.map (fun f -> lft_fconstr k f) v
let clos_rel e i =
match expand_rel i e with
@@ -452,7 +452,7 @@ let compact_stack head stk =
(* Put an update mark in the stack, only if needed *)
let zupdate m s =
- if !share & m.norm = Red
+ if !share && begin match m.norm with Red -> true | _ -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
@@ -760,7 +760,7 @@ let rec reloc_rargs_rec depth stk =
match stk with
Zapp args :: s ->
Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
- | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
+ | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s
| _ -> stk
let reloc_rargs depth stk =
@@ -771,13 +771,13 @@ let rec drop_parameters depth n argstk =
Zapp args::s ->
let q = Array.length args in
if n > q then drop_parameters depth (n-q) s
- else if n = q then reloc_rargs depth s
+ else if Int.equal n q then reloc_rargs depth s
else
let aft = Array.sub args n (q-n) in
reloc_rargs depth (append_stack aft s)
| Zshift(k)::s -> drop_parameters (depth-k) n s
| [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
- if n=0 then []
+ if Int.equal n 0 then []
else anomaly
"ill-typed term: found a match on a partially applied constructor"
| _ -> assert false
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b8edcae72..b995f2e4a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -127,7 +127,7 @@ let subst_const_def sub = function
| OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
let subst_const_body sub cb = {
- const_hyps = (assert (cb.const_hyps=[]); []);
+ const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
const_body = subst_const_def sub cb.const_body;
const_type = subst_const_type sub cb.const_type;
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
@@ -341,7 +341,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 = (match mib.mind_hyps with [] -> [] | _ -> assert false);
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 301c3b152..20436cbe7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -49,8 +49,9 @@ let named_context_val env = env.env_named_context,env.env_named_vals
let rel_context env = env.env_rel_context
let empty_context env =
- env.env_rel_context = empty_rel_context
- && env.env_named_context = empty_named_context
+ match env.env_rel_context, env.env_named_context with
+ | [], [] -> true
+ | _ -> false
(* Rel context *)
let lookup_rel n env =
@@ -321,7 +322,7 @@ let apply_to_hyp (ctxt,vals) id f =
let rec aux rtail ctxt vals =
match ctxt, vals with
| (idc,c,ct as d)::ctxt, v::vals ->
- if idc = id then
+ if id_eq idc id then
(f ctxt d rtail)::ctxt, v::vals
else
let ctxt',vals' = aux (d::rtail) ctxt vals in
@@ -334,7 +335,7 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
let rec aux ctxt vals =
match ctxt,vals with
| (idc,c,ct as d)::ctxt, v::vals ->
- if idc = id then
+ if id_eq idc id then
let sign = ctxt,vals in
push_named_context_val (f d sign) sign
else
@@ -348,7 +349,7 @@ let insert_after_hyp (ctxt,vals) id d check =
let rec aux ctxt vals =
match ctxt, vals with
| (idc,c,ct)::ctxt', v::vals' ->
- if idc = id then begin
+ if id_eq idc id then begin
check ctxt;
push_named_context_val d (ctxt,vals)
end else
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 30c2387ea..319f95c61 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -49,7 +49,7 @@ let rec reloc_rel n = function
let rec is_lift_id = function
| ELID -> true
- | ELSHFT(e,n) -> n=0 & is_lift_id e
+ | ELSHFT(e,n) -> Int.equal n 0 & is_lift_id e
| ELLFT (_,e) -> is_lift_id e
(*********************)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c53a0bcd9..a44afce2b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -190,7 +190,7 @@ let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
(* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
the situation where a non-Prop singleton inductive becomes Prop
when applied to Prop params *)
- if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort
+ if not polyprop && not (is_type0m_univ ar.poly_level) && is_prop_sort s
then raise (SingletonInductiveBecomesProp mip.mind_typename);
mkArity (List.rev ctx,s)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f2511dbde..a85395497 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -31,6 +31,8 @@ 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 find_mp mp map = MPmap.find mp (fst map)
@@ -391,10 +393,10 @@ let subst_mps sub c =
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
- | _ when mp = mpfrom -> mpto
+ | _ when mp_eq mp mpfrom -> mpto
| MPdot (mp1,l) ->
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
- if mp1==mp1' then mp
+ if mp1 == mp1' then mp
else MPdot (mp1',l)
| _ -> mp
@@ -406,7 +408,7 @@ let replace_mp_in_kn mpfrom mpto kn =
let rec mp_in_mp mp mp1 =
match mp1 with
- | _ when mp1 = mp -> true
+ | _ when mp_eq mp1 mp -> true
| MPdot (mp2,l) -> mp_in_mp mp mp2
| _ -> false
@@ -483,7 +485,7 @@ 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
@@ -522,13 +524,13 @@ let join subst1 subst2 =
Umap.join subst2 subst
let rec occur_in_path mbi = function
- | MPbound bid' -> mbi = bid'
+ | MPbound bid' -> mod_bound_id_eq mbi bid'
| MPdot (mp1,_) -> occur_in_path mbi mp1
| _ -> false
let occur_mbid mbi sub =
let check_one mbi' (mp,_) =
- if mbi = mbi' || occur_in_path mbi mp then raise Exit
+ if mod_bound_id_eq mbi mbi' || occur_in_path mbi mp then raise Exit
in
try
Umap.iter_mbi check_one sub;
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1bef6bf50..084628a4e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -138,10 +138,10 @@ let module_body_of_type mp mtb =
mod_retroknowledge = []}
let check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then () else
+ if mp_eq mp1 mp2 then () else
let mb1=lookup_module mp1 env in
let mb2=lookup_module mp2 env in
- if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2)
+ if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2)
then ()
else error_not_equal_modpaths mp1 mp2
@@ -184,7 +184,7 @@ and subst_structure sub do_delta sign =
and subst_module sub do_delta mb =
let mp = subst_mp sub mb.mod_mp in
- let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then
+ let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then
add_mp mb.mod_mp mp
empty_delta_resolver sub else sub in
let id_delta = (fun x y-> x) in
@@ -557,7 +557,7 @@ and clean_expr l = function
| SEBfunctor (mbid,sigt,str) as s->
let str_clean = clean_expr l str in
let sig_clean = clean_expr l sigt.typ_expr in
- if str_clean == str && sig_clean = sigt.typ_expr then
+ if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
| SEBstruct str as s->
let str_clean = Util.List.smartmap (clean_struct l) str in
diff --git a/kernel/names.ml b/kernel/names.ml
index 250b4a6b5..08b111cd6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -42,9 +42,9 @@ let id_of_string s =
let string_of_id id = String.copy id
-let id_ord (x : string) (y : string) =
- (* String.compare already checks for pointer equality *)
- String.compare x y
+let id_ord = String.compare
+
+let id_eq = String.equal
module IdOrdered =
struct
@@ -69,6 +69,11 @@ module Idpred = Predicate.Make(IdOrdered)
type name = Name of identifier | Anonymous
type variable = identifier
+let name_eq n1 n2 = match n1, n2 with
+| Anonymous, Anonymous -> true
+| Name id1, Name id2 -> String.equal id1 id2
+| _ -> false
+
(** {6 Directory paths = section names paths } *)
(** Dirpaths are lists of module identifiers.
@@ -134,6 +139,7 @@ module Umap = Map.Make(UOrdered)
type mod_bound_id = uniq_ident
let mod_bound_id_ord = uniq_ident_ord
+let mod_bound_id_eq mbl mbr = Int.equal (uniq_ident_ord mbl mbr) 0
let make_mbid = make_uid
let repr_mbid (n, id, dp) = (n, id, dp)
let debug_string_of_mbid = debug_string_of_uid
@@ -187,6 +193,8 @@ let rec mp_ord mp1 mp2 =
| MPbound _, MPdot _ -> -1
| MPdot _, _ -> 1
+let mp_eq mp1 mp2 = Int.equal (mp_ord mp1 mp2) 0
+
module MPord = struct
type t = module_path
let compare = mp_ord
@@ -214,7 +222,9 @@ let label kn =
let _,_,l = repr_kn kn in l
let string_of_kn (mp,dir,l) =
- let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#"
+ let str_dir = match dir with
+ | [] -> "."
+ | _ -> "#" ^ string_of_dirpath dir ^ "#"
in
string_of_mp mp ^ str_dir ^ string_of_label l
@@ -380,9 +390,10 @@ type evaluable_global_reference =
| EvalVarRef of identifier
| EvalConstRef of constant
-let eq_egr e1 e2 = match e1,e2 with
+let eq_egr e1 e2 = match e1, e2 with
EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
- | _,_ -> e1 = e2
+ | EvalVarRef id1, EvalVarRef id2 -> Int.equal (id_ord id1 id2) 0
+ | _, _ -> false
(** {6 Hash-consing of name objects } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 5c2bd5b0a..5ab3b5c3f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -18,6 +18,7 @@ val string_of_id : identifier -> string
val id_of_string : string -> identifier
val id_ord : identifier -> identifier -> int
+val id_eq : identifier -> identifier -> bool
(** Identifiers sets and maps *)
module Idset : Set.S with type elt = identifier
@@ -33,6 +34,8 @@ end
type name = Name of identifier | Anonymous
type variable = identifier
+val name_eq : name -> name -> bool
+
(** {6 Directory paths = section names paths } *)
type module_ident = identifier
@@ -71,6 +74,7 @@ module Labmap : Map.S with type key = label
type mod_bound_id
val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
(** The first argument is a file name - to prevent conflict between
different files *)
@@ -88,6 +92,9 @@ type module_path =
| MPbound of mod_bound_id
| MPdot of module_path * label
+val mp_ord : module_path -> module_path -> int
+val mp_eq : module_path -> module_path -> bool
+
val check_bound_mp : module_path -> bool
val string_of_mp : module_path -> string
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6e5a45b9c..207a37f97 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -116,7 +116,7 @@ let push_named d env =
env_named_vals = (id,rval):: env.env_named_vals }
let lookup_named_val id env =
- snd(List.find (fun (id',_) -> id = id') env.env_named_vals)
+ snd(List.find (fun (id',_) -> id_eq id id') env.env_named_vals)
(* Warning all the names should be different *)
let env_of_named id env = env
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1d974eada..b0ea2f7db 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -51,15 +51,15 @@ let el_stack el stk =
let compare_stack_shape stk1 stk2 =
let rec compare_rec bal stk1 stk2 =
match (stk1,stk2) with
- ([],[]) -> bal=0
+ ([],[]) -> Int.equal bal 0
| ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
| (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
| (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
- bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
+ Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
- bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+ Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
| (_,_) -> false in
compare_rec 0 stk1 stk2
@@ -181,14 +181,18 @@ type conv_pb =
| CONV
| CUMUL
+let is_cumul = function CUMUL -> true | CONV -> false
+
let sort_cmp pb s0 s1 cuniv =
match (s0,s1) with
- | (Prop c1, Prop c2) when pb = CUMUL ->
- if c1 = Null or c2 = Pos then cuniv (* Prop <= Set *)
- else raise NotConvertible
+ | (Prop c1, Prop c2) when is_cumul pb ->
+ begin match c1, c2 with
+ | Null, _ | _, Pos -> cuniv (* Prop <= Set *)
+ | _ -> raise NotConvertible
+ end
| (Prop c1, Prop c2) ->
- if c1 = c2 then cuniv else raise NotConvertible
- | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
+ if c1 == c2 then cuniv else raise NotConvertible
+ | (Prop c1, Type u) when is_cumul pb -> assert (is_univ_variable u); cuniv
| (Type u1, Type u2) ->
assert (is_univ_variable u2);
(match pb with
@@ -266,12 +270,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly "conversion was given ill-typed terms (Sort)";
sort_cmp cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
- if n=m
+ if Int.equal n m
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| _ -> raise NotConvertible)
| (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
- if ev1=ev2 then
+ if Int.equal ev1 ev2 then
let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
convert_vect l2r infos el1 el2
(Array.map (mk_clos env1) args1)
@@ -280,7 +284,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
- if reloc_rel n el1 = reloc_rel m el2
+ if Int.equal (reloc_rel n el1) (reloc_rel m el2)
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -362,13 +366,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
else raise NotConvertible
| (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
- if j1 = j2 && eq_ind ind1 ind2
+ if Int.equal j1 j2 && eq_ind ind1 ind2
then
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
- if op1 = op2
+ | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
+ if Int.equal i1 i2 && Array.equal Int.equal op1 op2
then
let n = Array.length cl1 in
let fty1 = Array.map (mk_clos e1) tys1 in
@@ -383,7 +387,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
else raise NotConvertible
| (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
- if op1 = op2
+ if Int.equal op1 op2
then
let n = Array.length cl1 in
let fty1 = Array.map (mk_clos e1) tys1 in
@@ -414,7 +418,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
let lv2 = Array.length v2 in
- if lv1 = lv2
+ if Int.equal lv1 lv2
then
let rec fold n univ =
if n >= lv1 then univ
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 269f7a5d9..b2a509678 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -29,7 +29,7 @@ let empty_named_context = []
let add_named_decl d sign = d::sign
let rec lookup_named id = function
- | (id',_,_ as decl) :: _ when id=id' -> decl
+ | (id',_,_ as decl) :: _ when id_eq id id' -> decl
| _ :: sign -> lookup_named id sign
| [] -> raise Not_found
diff --git a/kernel/term.ml b/kernel/term.ml
index a99262adf..94aa7d968 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -63,6 +63,10 @@ let prop_sort = Prop Null
let set_sort = Prop Pos
let type1_sort = Type type1_univ
+let is_prop_sort = function
+| Prop Null -> true
+| _ -> false
+
type sorts_family = InProp | InSet | InType
let family_of_sort = function
@@ -138,7 +142,7 @@ let mkSort = function
(* (that means t2 is declared as the type of t1) *)
let mkCast (t1,k2,t2) =
match t1 with
- | Cast (c,k1, _) when k1 = VMcast & k1 = k2 -> Cast (c,k1,t2)
+ | Cast (c,k1, _) when k1 == VMcast && k1 == k2 -> Cast (c,k1,t2)
| _ -> Cast (t1,k2,t2)
(* Constructs the product (x:t1)t2 *)
@@ -265,7 +269,7 @@ let destMeta c = match kind_of_term c with
| _ -> invalid_arg "destMeta"
let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-let isMetaOf mv c = match kind_of_term c with Meta mv' -> mv = mv' | _ -> false
+let isMetaOf mv c = match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
(* Destructs a variable *)
let destVar c = match kind_of_term c with
@@ -324,11 +328,11 @@ let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
(* Tests if a de Bruijn index *)
let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
-let isRelN n c = match kind_of_term c with Rel n' -> n = n' | _ -> false
+let isRelN n c = match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
(* Tests if a variable *)
let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c = match kind_of_term c with Var id' -> id = id' | _ -> false
+let isVarId id c = match kind_of_term c with Var id' -> Int.equal (id_ord id id') 0 | _ -> false
(* Tests if an inductive *)
let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
@@ -559,30 +563,31 @@ let map_constr_with_binders g f l c = match kind_of_term c with
let compare_constr f t1 t2 =
match kind_of_term t1, kind_of_term 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 -> Int.equal (id_ord id1 id2) 0
+ | Sort s1, Sort s2 -> Int.equal (Pervasives.compare s1 s2) 0 (** FIXME **)
| 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), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2
| _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
| App (c1,l1), App (c2,l2) ->
- Array.length l1 = Array.length l2 &&
- f c1 c2 && Array.for_all2 f l1 l2
- | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
+ Int.equal (Array.length l1) (Array.length l2) &&
+ f c1 c2 && Array.equal f l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
| Const c1, Const c2 -> eq_constant c1 c2
| Ind c1, Ind c2 -> eq_ind c1 c2
| Construct c1, Construct c2 -> eq_constructor 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
(*******************************)
@@ -592,21 +597,20 @@ let compare_constr f t1 t2 =
(* alpha conversion : ignore print names and casts *)
let rec eq_constr m n =
- (m==n) or
- compare_constr eq_constr m n
+ (m == n) || compare_constr eq_constr m n
let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
let constr_ord_int f t1 t2 =
let (=?) f g i1 i2 j1 j2=
- let c=f i1 i2 in
- if c=0 then g j1 j2 else c in
+ let c = f i1 i2 in
+ if Int.equal c 0 then g j1 j2 else c in
let (==?) fg h i1 i2 j1 j2 k1 k2=
let c=fg i1 i2 j1 j2 in
- if c=0 then h k1 k2 else c in
+ if Int.equal c 0 then h k1 k2 else c in
match kind_of_term t1, kind_of_term t2 with
- | Rel n1, Rel n2 -> n1 - n2
- | Meta m1, Meta m2 -> m1 - m2
+ | Rel n1, Rel n2 -> Int.compare n1 n2
+ | Meta m1, Meta m2 -> Int.compare m1 m2
| Var id1, Var id2 -> id_ord id1 id2
| Sort s1, Sort s2 -> Pervasives.compare s1 s2
| Cast (c1,_,_), _ -> f c1 t2
@@ -671,7 +675,7 @@ let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
- n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+ name_eq n1 n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
(***************************************************************************)
(* Type of local contexts (telescopes) *)
@@ -729,7 +733,7 @@ let closed0 = closedn 0
let noccurn n term =
let rec occur_rec n c = match kind_of_term 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
@@ -839,7 +843,7 @@ let subst1_named_decl = subst1_decl
let rec thin_val = function
| [] -> []
| (((id,{ sit = v }) as s)::tl) when isVar v ->
- if id = destVar v then thin_val tl else s::(thin_val tl)
+ if Int.equal (id_ord id (destVar v)) 0 then thin_val tl else s::(thin_val tl)
| h::tl -> h::(thin_val tl)
(* (replace_vars sigma M) applies substitution sigma to term M *)
@@ -853,7 +857,9 @@ let replace_vars var_alist =
with Not_found -> c)
| _ -> map_constr_with_binders succ substrec n c
in
- if var_alist = [] then (function x -> x) else substrec 0
+ match var_alist with
+ | [] -> (function x -> x)
+ | _ -> substrec 0
(*
let repvarkey = Profile.declare_profile "replace_vars";;
@@ -1017,7 +1023,7 @@ let decompose_lam =
let decompose_prod_n n =
if n < 0 then error "decompose_prod_n: 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 kind_of_term c with
| Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
@@ -1030,7 +1036,7 @@ let decompose_prod_n n =
let decompose_lam_n n =
if n < 0 then error "decompose_lam_n: 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 kind_of_term c with
| Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
| Cast (c,_,_) -> lamdec_rec l n c
@@ -1068,7 +1074,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 kind_of_term c with
| Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
@@ -1085,7 +1091,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 kind_of_term c with
| Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
@@ -1199,9 +1205,9 @@ let rec isArity c =
let array_eqeq t1 t2 =
t1 == t2 ||
- (Array.length t1 = Array.length t2 &&
+ (Int.equal (Array.length t1) (Array.length t2) &&
let rec aux i =
- (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1))
+ (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
in aux 0)
let equals_constr t1 t2 =
@@ -1216,20 +1222,21 @@ let equals_constr t1 t2 =
| LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
| App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2
- | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_eqeq l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2
| Const c1, Const c2 -> c1 == c2
- | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 & i1 = i2
+ | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2
| Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) ->
- sp1 == sp2 & i1 = i2 & j1 = j2
+ sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2
| Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2
- | Fix (ln1,(lna1,tl1,bl1)), Fix (ln2,(lna2,tl2,bl2)) ->
- ln1 = ln2
- & array_eqeq lna1 lna2
- & array_eqeq tl1 tl2
- & array_eqeq bl1 bl2
+ | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
+ Int.equal i1 i2
+ && Array.equal Int.equal ln1 ln2
+ && array_eqeq lna1 lna2
+ && array_eqeq tl1 tl2
+ && array_eqeq bl1 bl2
| CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) ->
- ln1 = ln2
+ Int.equal ln1 ln2
& array_eqeq lna1 lna2
& array_eqeq tl1 tl2
& array_eqeq bl1 bl2
@@ -1379,7 +1386,7 @@ module Hsorts =
| Type u -> Type (huniv u)
let equal s1 s2 =
match (s1,s2) with
- (Prop c1, Prop c2) -> c1=c2
+ (Prop c1, Prop c2) -> c1 == c2
| (Type u1, Type u2) -> u1 == u2
|_ -> false
let hash = Hashtbl.hash
@@ -1391,11 +1398,14 @@ module Hcaseinfo =
type t = case_info
type u = inductive -> inductive
let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
+ let pp_info_equal info1 info2 =
+ Int.equal info1.ind_nargs info2.ind_nargs &&
+ info1.style == info2.style
let equal ci ci' =
ci.ci_ind == ci'.ci_ind &&
- ci.ci_npar = ci'.ci_npar &&
- ci.ci_cstr_ndecls = ci'.ci_cstr_ndecls && (* we use (=) on purpose *)
- ci.ci_pp_info = ci'.ci_pp_info (* we use (=) on purpose *)
+ Int.equal ci.ci_npar ci'.ci_npar &&
+ Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+ pp_info_equal ci.ci_pp_info ci'.ci_pp_info (* we use (=) on purpose *)
let hash = Hashtbl.hash
end)
diff --git a/kernel/term.mli b/kernel/term.mli
index 15fcdd189..85192e1f1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -21,6 +21,8 @@ val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
+val is_prop_sort : sorts -> bool
+
(** {6 The sorts family of CCI. } *)
type sorts_family = InProp | InSet | InType
diff --git a/kernel/univ.ml b/kernel/univ.ml
index bdd668cbd..18bee0fb4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -557,7 +557,7 @@ type constraint_function =
let constraint_add_leq v u c =
(* We just discard trivial constraints like Set<=u or u<=u *)
- if v = UniverseLevel.Set || UniverseLevel.equal v u then c
+ if UniverseLevel.equal v UniverseLevel.Set || UniverseLevel.equal v u then c
else Constraint.add (v,Le,u) c
let enforce_leq u v c =
@@ -634,12 +634,16 @@ let normalize_universes g =
let check_sorted g sorted =
let get u = try UniverseLMap.find u sorted with
| Not_found -> assert false
- in UniverseLMap.iter (fun u arc -> let lu = get u in match arc with
- | Equiv v -> assert (lu = get v)
- | Canonical {univ=u'; lt=lt; le=le} ->
+ in
+ let iter u arc =
+ let lu = get u in match arc with
+ | Equiv v -> assert (Int.equal lu (get v))
+ | Canonical {univ = u'; lt = lt; le = le} ->
assert (u == u');
List.iter (fun v -> assert (lu <= get v)) le;
- List.iter (fun v -> assert (lu < get v)) lt) g
+ List.iter (fun v -> assert (lu < get v)) lt
+ in
+ UniverseLMap.iter iter g
(**
Bellman-Ford algorithm with a few customizations:
@@ -648,7 +652,10 @@ let check_sorted g sorted =
vertices, and [bottom] is used as the source vertex
*)
let bellman_ford bottom g =
- assert (lookup_level bottom g = None);
+ let () = match lookup_level bottom g with
+ | None -> ()
+ | Some _ -> assert false
+ in
let ( << ) a b = match a, b with
| _, None -> true
| None, _ -> false
@@ -790,11 +797,11 @@ let make_max = function
| (le,lt) -> Max (le,lt)
let remove_large_constraint u = function
- | Atom u' as x -> if u = u' then Max ([],[]) else x
+ | Atom u' as x -> if UniverseLevel.equal u u' then Max ([],[]) else x
| Max (le,lt) -> make_max (List.remove u le,lt)
let is_direct_constraint u = function
- | Atom u' -> u = u'
+ | Atom u' -> UniverseLevel.equal u u'
| Max (le,lt) -> List.mem u le
(*
@@ -854,7 +861,7 @@ let no_upper_constraints u cst =
let univ_depends u v =
match u, v with
- | Atom u, Atom v -> u = v
+ | Atom u, Atom v -> UniverseLevel.equal u v
| Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
| _ -> anomaly "univ_depends given a non-atomic 1st arg"
@@ -948,7 +955,7 @@ module Hconstraint =
type u = universe_level -> universe_level
let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
let equal (l1,k,l2) (l1',k',l2') =
- l1 == l1' && k = k' && l2 == l2'
+ l1 == l1' && k == k' && l2 == l2'
let hash = Hashtbl.hash
end)
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 4615ad038..a5e38534f 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -102,7 +102,9 @@ let compare item_cmp v1 v2 =
cmp (Array.length v1 - 1)
let equal cmp t1 t2 =
- Array.length t1 = Array.length t2 &&
+ if t1 == t2 then true else
+ if not (Array.length t1 = Array.length t2) then false
+ else
let rec aux i =
(i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
in aux 0
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 130bbcf2f..556881332 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -36,7 +36,7 @@ let rec lift_rtree_rec depth n = function
| Rec(j,defs) ->
Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs)
-let lift n t = if n=0 then t else lift_rtree_rec 0 n t
+let lift n t = if Int.equal n 0 then t else lift_rtree_rec 0 n t
(* The usual subst operation *)
let rec subst_rtree_rec depth sub = function
@@ -153,12 +153,21 @@ let compare_rtree f = fold2
if b < 0 then false
else if b > 0 then true
else match expand t1, expand t2 with
- Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 ->
+ Node(_,v1), Node(_,v2) when Int.equal (Array.length v1) (Array.length v2) ->
Array.for_all2 cmp v1 v2
| _ -> false)
+let rec raw_eq cmp t1 t2 = match t1, t2 with
+| Param (i1, j1), Param (i2, j2) ->
+ Int.equal i1 i2 && Int.equal j1 j2
+| Node (x1, a1), Node (x2, a2) ->
+ cmp x1 x2 && Array.equal (raw_eq cmp) a1 a2
+| Rec (i1, a1), Rec (i2, a2) ->
+ Int.equal i1 i2 && Array.equal (raw_eq cmp) a1 a2
+| _ -> false
+
let eq_rtree cmp t1 t2 =
- t1 == t2 || t1=t2 ||
+ t1 == t2 || raw_eq cmp t1 t2 ||
compare_rtree
(fun t1 t2 ->
if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
@@ -175,8 +184,8 @@ let rec pp_tree prl t =
hov 2 (str"("++prl lab++str","++brk(1,0)++
prvect_with_sep pr_comma (pp_tree prl) v++str")")
| Rec(i,v) ->
- if Array.length v = 0 then str"Rec{}"
- else if Array.length v = 1 then
+ if Int.equal (Array.length v) 0 then str"Rec{}"
+ else if Int.equal (Array.length v) 1 then
hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}")
else
hov 2 (str"Rec{"++int i++str","++brk(1,0)++
diff --git a/lib/system.ml b/lib/system.ml
index 84706d031..a2b371b1f 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -24,7 +24,7 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
let ok_dirname f =
f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
- (Unicode.ident_refutation f = None)
+ (match Unicode.ident_refutation f with None -> true | _ -> false)
let all_subdirs ~unix_path:root =
let l = ref [] in
@@ -37,11 +37,13 @@ let all_subdirs ~unix_path:root =
if ok_dirname f then
let file = Filename.concat dir f in
try
- if (stat file).st_kind = S_DIR then begin
- let newrel = rel@[f] in
+ begin match (stat file).st_kind with
+ | S_DIR ->
+ let newrel = rel @ [f] in
add file newrel;
traverse file newrel
- end
+ | _ -> ()
+ end
with Unix_error (e,s1,s2) -> ()
done
with End_of_file ->
diff --git a/lib/util.ml b/lib/util.ml
index fcbd969ab..8d8c947c7 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -29,7 +29,7 @@ let pi3 (_,_,a) = a
let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
let is_digit c = (c >= '0' && c <= '9')
let is_ident_tail c =
- is_letter c or is_digit c or c = '\'' or c = '_'
+ is_letter c or is_digit c || c = '\'' or c = '_'
let is_blank = function
| ' ' | '\r' | '\t' | '\n' -> true
| _ -> false
diff --git a/library/libnames.ml b/library/libnames.ml
index a07895eec..e51e2c81c 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -50,21 +50,25 @@ let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if n = len && n > 0 then error (s ^ " is an invalid path.");
+ if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
- if pos = n then error (s ^ " is an invalid path.");
+ if Int.equal pos n then error (s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
in
decoupe_dirs [] 0
let dirpath_of_string s =
- make_dirpath (if s = "" then [] else parse_dir s)
+ let path = match s with
+ | "" -> []
+ | _ -> parse_dir s
+ in
+ make_dirpath path
let string_of_dirpath = Names.string_of_dirpath
@@ -85,8 +89,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
(* parsing and printing of section paths *)
let string_of_path sp =
let (sl,id) = repr_path sp in
- if repr_dirpath sl = [] then string_of_id id
- else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+ match repr_dirpath sl with
+ | [] -> string_of_id id
+ | _ -> (string_of_dirpath sl) ^ "." ^ (string_of_id id)
let sp_ord sp1 sp2 =
let (p1,id1) = repr_path sp1
diff --git a/library/nameops.ml b/library/nameops.ml
index 5ea7e2685..62665e8af 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -28,16 +28,16 @@ let cut_ident skip_quote s =
let slen = String.length s in
(* [n'] is the position of the first non nullary digit *)
let rec numpart n n' =
- if n = 0 then
+ if Int.equal n 0 then
(* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
slen
else
let c = Char.code (String.get s (n-1)) in
- if c = code_of_0 && n <> slen then
+ if Int.equal c code_of_0 && n <> slen then
numpart (n-1) n'
else if code_of_0 <= c && c <= code_of_9 then
numpart (n-1) (n-1)
- else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+ else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
numpart (n-1) (n-1)
else
n'
@@ -48,7 +48,7 @@ let repr_ident s =
let numstart = cut_ident false s in
let s = string_of_id s in
let slen = String.length s in
- if numstart = slen then
+ if Int.equal numstart slen then
(s, None)
else
(String.sub s 0 numstart,
@@ -75,7 +75,7 @@ let lift_subscript id =
let rec add carrypos =
let c = id.[carrypos] in
if is_digit c then
- if c = '9' then begin
+ if Int.equal (Char.code c) (Char.code '9') then begin
assert (carrypos>0);
add (carrypos-1)
end
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a60d9c966..b77c85bf7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -79,7 +79,7 @@ let check_for_coloneq =
let rec skip_to_rpar p n =
match get_tok (List.last (Stream.npeek n strm)) with
| KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
- | KEYWORD ")" -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
+ | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
| KEYWORD "." -> err ()
| _ -> skip_to_rpar p (n+1) in
let rec skip_names n =
@@ -127,11 +127,13 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
(id,CProdN(loc,bl,ty))
(* Functions overloaded by quotifier *)
-let induction_arg_of_constr (c,lbind as clbind) =
- if lbind = NoBindings then
- try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
- with _ -> ElimOnConstr clbind
- else ElimOnConstr clbind
+let induction_arg_of_constr (c,lbind as clbind) = match lbind with
+ | NoBindings ->
+ begin
+ try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
+ with _ -> ElimOnConstr clbind
+ end
+ | _ -> ElimOnConstr clbind
let mkTacCase with_evar = function
| [ElimOnConstr cl,(None,None)],None,None ->
@@ -158,10 +160,10 @@ let rec mkCLambdaN_simple_loc loc bll c =
| ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
| [] -> c
-let mkCLambdaN_simple bl c =
- if bl=[] then c
- else
- let loc = Loc.merge (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in
+let mkCLambdaN_simple bl c = match bl with
+ | [] -> c
+ | h :: _ ->
+ let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
mkCLambdaN_simple_loc loc bl c
let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l))
@@ -173,30 +175,41 @@ let map_int_or_var f = function
let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
let has_no_specified_occs cl =
- (cl.onhyps = None ||
- List.for_all (fun ((occs,_),_) -> occs = AllOccurrences)
- (Option.get cl.onhyps))
- && (cl.concl_occs = AllOccurrences
- || cl.concl_occs = NoOccurrences)
+ let forall ((occs, _), _) = match occs with
+ | AllOccurrences -> true
+ | _ -> false
+ in
+ let hyps = match cl.onhyps with
+ | None -> true
+ | Some hyps -> List.for_all forall hyps in
+ let concl = match cl.concl_occs with
+ | AllOccurrences | NoOccurrences -> true
+ | _ -> false
+ in
+ hyps && concl
let merge_occurrences loc cl = function
| None ->
if has_no_specified_occs cl then (None, cl)
else
user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
- | Some (occs,p) ->
- (Some p,
- if occs = AllOccurrences then cl
- else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs }
- else match cl.onhyps with
- | Some [(occs',id),l] when
- occs' = AllOccurrences && cl.concl_occs = NoOccurrences ->
- { cl with onhyps=Some[(occs,id),l] }
+ | Some (occs, p) ->
+ let ans = match occs with
+ | AllOccurrences -> cl
+ | _ ->
+ begin match cl with
+ | { onhyps = Some []; concl_occs = AllOccurrences } ->
+ { onhyps = Some []; concl_occs = occs }
+ | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } ->
+ { cl with onhyps = Some [(occs, id), l] }
| _ ->
- if has_no_specified_occs cl then
- user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
- else
- user_err_loc (loc,"",str "Cannot use clause \"at\" twice."))
+ if has_no_specified_occs cl then
+ user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+ else
+ user_err_loc (loc,"",str "Cannot use clause \"at\" twice.")
+ end
+ in
+ (Some p, ans)
(* Auxiliary grammar rules *)
@@ -612,7 +625,9 @@ GEXTEND Gram
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
- | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
+ | IDENT "clear"; l = LIST0 id_or_meta ->
+ let is_empty = match l with [] -> true | _ -> false in
+ TacClear (is_empty, l)
| IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
| IDENT "move"; hfrom = id_or_meta; hto = move_location ->
TacMove (true,hfrom,hto)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 29b3579f0..377da0bdf 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -85,7 +85,11 @@ let uri_of_data s =
let n = String.index s ':' in
let p = String.index s '.' in
let s = String.sub s (n+2) (p-n-2) in
- for i=0 to String.length s - 1 do if s.[i]='/' then s.[i]<-'.' done;
+ for i = 0 to String.length s - 1 do
+ match s.[i] with
+ | '/' -> s.[i] <- '.'
+ | _ -> ()
+ done;
qualid_of_string s
let constant_of_cdata (loc,a) = Nametab.locate_constant (uri_of_data a)
@@ -201,7 +205,7 @@ let rec interp_xml_constr = function
user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
and interp_xml_tag s = function
- | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl)
+ | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
| XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 3071e0eb4..80940b4d3 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -137,16 +137,16 @@ let check_utf8_trailing_byte cs c =
(* but don't certify full utf8 compliance (e.g. no emptyness check) *)
let lookup_utf8_tail c cs =
let c1 = Char.code c in
- if c1 land 0x40 = 0 or c1 land 0x38 = 0x38 then error_utf8 cs
+ if Int.equal (c1 land 0x40) 0 or Int.equal (c1 land 0x38) 0x38 then error_utf8 cs
else
let n, unicode =
- if c1 land 0x20 = 0 then
+ if Int.equal (c1 land 0x20) 0 then
match Stream.npeek 2 cs with
| [_;c2] ->
check_utf8_trailing_byte cs c2;
2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F)
| _ -> error_utf8 cs
- else if c1 land 0x10 = 0 then
+ else if Int.equal (c1 land 0x10) 0 then
match Stream.npeek 3 cs with
| [_;c2;c3] ->
check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3;
@@ -281,8 +281,11 @@ let rec string in_comments bp len = parser
| [< ''*'; s >] ->
(parser
| [< '')'; s >] ->
- if in_comments = Some 0 then
- msg_warning (strbrk "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.");
+ let () = match in_comments with
+ | Some 0 ->
+ msg_warning (strbrk "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.")
+ | _ -> ()
+ in
let in_comments = Option.map pred in_comments in
string in_comments bp (store (store len '*') ')') s
| [< >] ->
@@ -296,7 +299,9 @@ let set_xml_output_comment f = xml_output_comment := f
(* Utilities for comments in beautify *)
let comment_begin = ref None
-let comm_loc bp = if !comment_begin=None then comment_begin := Some bp
+let comm_loc bp = match !comment_begin with
+| None -> comment_begin := Some bp
+| _ -> ()
let current = Buffer.create 8192
let between_com = ref true
@@ -319,7 +324,7 @@ let push_char c =
if
!between_com || List.mem c ['\n';'\r'] ||
(List.mem c [' ';'\t']&&
- (Buffer.length current = 0 ||
+ (Int.equal (Buffer.length current) 0 ||
not (let s = Buffer.contents current in
List.mem s.[String.length s - 1] [' ';'\t';'\n';'\r'])))
then
@@ -354,8 +359,11 @@ let rec comm_string bp = parser
| [< ''"' >] -> push_string "\""
| [< ''\\'; _ =
(parser [< ' ('"' | '\\' as c) >] ->
- if c='"' then real_push_char c;
- real_push_char c
+ let () = match c with
+ | '"' -> real_push_char c
+ | _ -> ()
+ in
+ real_push_char c
| [< >] -> real_push_char '\\'); s >]
-> comm_string bp s
| [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
@@ -399,11 +407,11 @@ and update_longest_valid_token last nj tt cs =
and progress_utf8 last nj n c tt cs =
try
let tt = CharMap.find c tt.branch in
- if n=1 then
+ if Int.equal n 1 then
update_longest_valid_token last (nj+n) tt cs
else
match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
- | l when List.length l = n-1 ->
+ | l when Int.equal (List.length l) (n - 1) ->
List.iter (check_utf8_trailing_byte cs) l;
let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
update_longest_valid_token last (nj+n) tt cs
@@ -477,10 +485,12 @@ let rec next_token = parser bp
comment_stop bp;
(* We enforce that "." should either be part of a larger keyword,
for instance ".(", or followed by a blank or eof. *)
- if t = KEYWORD "." then begin
+ let () = match t with
+ | KEYWORD "." ->
if not (blank_or_eof s) then err (bp,ep+1) Undefined_token;
if Flags.do_beautify() then between_com := true;
- end;
+ | _ -> ()
+ in
(t, (bp,ep))
| [< ''?'; s >] ep ->
let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
@@ -631,14 +641,14 @@ let is_ident_not_keyword s =
let is_number s =
let rec aux i =
- String.length s = i or
+ Int.equal (String.length s) i ||
match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
in aux 0
let strip s =
let len =
let rec loop i len =
- if i = String.length s then len
+ if Int.equal i (String.length s) then len
else if s.[i] == ' ' then loop (i + 1) len
else loop (i + 1) (len + 1)
in
@@ -656,7 +666,7 @@ let strip s =
let terminal s =
let s = strip s in
- if s = "" then failwith "empty token";
+ let () = match s with "" -> failwith "empty token" | _ -> () in
if is_ident_not_keyword s then IDENT s
else if is_number s then INT s
else KEYWORD s
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b14822b8a..66b248cb0 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -164,9 +164,9 @@ let grammar_delete e reinit (pos,rls) =
(List.rev rls);
if reinit <> None then
let lev = match pos with Some (Level n) -> n | _ -> assert false in
- let pos =
- if lev = "200" then First
- else After (string_of_int (int_of_string lev + 1)) in
+ let pos = match lev with
+ | "200" -> First
+ | _ -> After (string_of_int (int_of_string lev + 1)) in
maybe_uncurry (G.extend e) (Some pos, [Some lev,reinit,[]])
(** The apparent parser of Coq; encapsulate G to keep track
@@ -502,7 +502,7 @@ let find_position_gen forpat ensure assoc lev =
let init = ref None in
let rec add_level q = function
| (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
- | (p,a,reinit)::l when p = n ->
+ | (p,a,reinit)::l when Int.equal p n ->
if reinit then
let a' = create_assoc assoc in (init := Some a'; (p,a',false)::l)
else if admissible_assoc (a,assoc) then
@@ -517,14 +517,19 @@ let find_position_gen forpat ensure assoc lev =
else (add_level None ccurrent, pcurrent) in
level_stack := updated:: !level_stack;
let assoc = create_assoc assoc in
- if !init = None then
+ begin match !init with
+ | None ->
(* Create the entry *)
- (if !after = None then Some Extend.First
- else Some (Extend.After (constr_level (Option.get !after)))),
- Some assoc, Some (constr_level n), None
- else
+ let ext = match !after with
+ | None -> Some Extend.First
+ | _ ->
+ Some (Extend.After (constr_level (Option.get !after)))
+ in
+ ext, Some assoc, Some (constr_level n), None
+ | _ ->
(* The reinit flag has been updated *)
Some (Extend.Level (constr_level n)), None, None, !init
+ end
with
(* Nothing has changed *)
Exit ->
@@ -537,7 +542,7 @@ let remove_levels n =
let rec list_mem_assoc_triple x = function
| [] -> false
- | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
+ | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l
let register_empty_levels forpat levels =
let filter n =
@@ -565,6 +570,12 @@ let camlp4_assoc = function
| Some Extend.NonA | Some Extend.RightA -> Extend.RightA
| None | Some Extend.LeftA -> Extend.LeftA
+let assoc_eq al ar = match al, ar with
+| Extend.NonA, Extend.NonA
+| Extend.RightA, Extend.RightA
+| Extend.LeftA, Extend.LeftA -> true
+| _, _ -> false
+
(* [adjust_level assoc from prod] where [assoc] and [from] are the name
and associativity of the level where to add the rule; the meaning of
the result is
@@ -587,18 +598,21 @@ let adjust_level assoc from = function
(* If NonA on the left-hand side, adopt the current assoc ?? *)
| (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None
(* If the expected assoc is the current one, set to SELF *)
- | (NumLevel n,BorderProd (Left,Some a)) when a = camlp4_assoc assoc ->
+ | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) ->
None
(* Otherwise, force the level, n or n-1, according to expected assoc *)
| (NumLevel n,BorderProd (Left,Some a)) ->
- if a = Extend.LeftA then Some (Some (n,true)) else Some None
+ begin match a with
+ | Extend.LeftA -> Some (Some (n, true))
+ | _ -> Some None
+ end
(* None means NEXT *)
| (NextLevel,_) -> Some None
(* Compute production name elsewhere *)
| (NumLevel n,InternalProd) ->
match from with
- | ETConstr (p,()) when p = n+1 -> Some None
- | ETConstr (p,()) -> Some (Some (n,n=p))
+ | ETConstr (p,()) when Int.equal p (n + 1) -> Some None
+ | ETConstr (p,()) -> Some (Some (n, Int.equal n p))
| _ -> Some (Some (n,false))
let compute_entry allow_create adjust forpat = function
@@ -610,7 +624,8 @@ let compute_entry allow_create adjust forpat = function
| ETBinder true -> anomaly "Should occur only as part of BinderList"
| ETBinder false -> weaken_entry Constr.binder, None, false
| ETBinderList (true,tkl) ->
- assert (tkl=[]); weaken_entry Constr.open_binders, None, false
+ let () = match tkl with [] -> () | _ -> assert false in
+ weaken_entry Constr.open_binders, None, false
| ETBinderList (false,_) -> anomaly "List of entries cannot be registered."
| ETBigint -> weaken_entry Prim.bigint, None, false
| ETReference -> weaken_entry Constr.global, None, false
@@ -643,10 +658,11 @@ let is_self from e =
match from, e with
ETConstr(n,()), ETConstr(NumLevel n',
BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false
- | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> n=n'
+ | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n'
| (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
| ETPattern, ETPattern) -> true
- | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2'
+ | ETOther(s1,s2), ETOther(s1',s2') ->
+ Int.equal (String.compare s1 s1') 0 && Int.equal (String.compare s2 s2') 0
| _ -> false
let is_binder_level from e =
@@ -726,33 +742,49 @@ let level_of_snterml = function
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
+let coincide s pat off =
+ let len = String.length pat in
+ let break = ref true in
+ let i = ref 0 in
+ while !break && !i < len do
+ let c = Char.code s.[off + !i] in
+ let d = Char.code pat.[!i] in
+ break := Int.equal c d;
+ incr i
+ done;
+ !break
+
let rec interp_entry_name static up_level s sep =
let l = String.length s in
- if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
+ if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
let t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
List1ArgType t, Alist1 g
- else if l > 12 & String.sub s 0 3 = "ne_" &
- String.sub s (l-9) 9 = "_list_sep" then
+ else if l > 12 && coincide s "ne_" 0 &&
+ coincide s "_list_sep" (l-9) then
let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
List1ArgType t, Alist1sep (g,sep)
- else if l > 5 & String.sub s (l-5) 5 = "_list" then
+ else if l > 5 && coincide s "_list" (l-5) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
List0ArgType t, Alist0 g
- else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then
+ else if l > 9 && coincide s "_list_sep" (l-9) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
List0ArgType t, Alist0sep (g,sep)
- else if l > 4 & String.sub s (l-4) 4 = "_opt" then
+ else if l > 4 && coincide s "_opt" (l-4) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
OptArgType t, Aopt g
- else if l > 5 & String.sub s (l-5) 5 = "_mods" then
+ else if l > 5 && coincide s "_mods" (l-5) then
let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
List0ArgType t, Amodifiers g
else
- let s = if s = "hyp" then "var" else s in
+ let s = match s with "hyp" -> "var" | _ -> s in
+ let check_lvl n = match up_level with
+ | None -> false
+ | Some m -> Int.equal m n && not (Int.equal m 5)
+ in
let t, se =
match Extrawit.tactic_genarg_level s with
- | Some n when Some n = up_level & up_level <> Some 5 -> None, Aself
- | Some n when Some (n+1) = up_level & up_level <> Some 5 -> None, Anext
+ | Some n when check_lvl n -> None, Aself
+ | Some n when check_lvl (n + 1) -> None, Anext
| Some n -> None, Atactic n
| None ->
try Some (get_entry uprim s), Aentry ("prim",s) with Not_found ->
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index c3726f1a8..f823cfa55 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -87,7 +87,7 @@ let value i t=
let add x y=
if x<0 then y else if y<0 then x else x+y in
let rec vaux term=
- if isMeta term && destMeta term = i then 0 else
+ if isMeta term && Int.equal (destMeta term) i then 0 else
let f v t=add v (vaux t) in
let vr=fold_constr f (-1) term in
if vr<0 then -1 else vr+1 in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 01:23:26 +0000