aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--toplevel/auto_ind_decl.ml32
-rw-r--r--toplevel/autoinstance.ml5
-rw-r--r--toplevel/backtrack.ml11
-rw-r--r--toplevel/cerrors.ml18
-rw-r--r--toplevel/class.ml6
-rw-r--r--toplevel/classes.ml31
-rw-r--r--toplevel/command.ml48
-rw-r--r--toplevel/coqinit.ml1
-rw-r--r--toplevel/coqtop.ml12
-rw-r--r--toplevel/himsg.ml20
-rw-r--r--toplevel/ide_slave.ml4
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml12
-rw-r--r--toplevel/lemmas.ml29
-rw-r--r--toplevel/metasyntax.ml154
-rw-r--r--toplevel/mltop.ml2
-rw-r--r--toplevel/obligations.ml33
-rw-r--r--toplevel/record.ml18
-rw-r--r--toplevel/search.ml22
-rw-r--r--toplevel/toplevel.ml18
-rw-r--r--toplevel/vernac.ml7
-rw-r--r--toplevel/vernacentries.ml74
22 files changed, 306 insertions, 253 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index fa5dce73f..3fc4aa84f 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -189,7 +189,7 @@ let build_beq_scheme kn =
in
let args = Array.append
(Array.map (fun x->lift lifti x) a) eqa
- in if args = [||] then eq
+ in if Array.equal eq_constr args [||] then eq
else mkApp (eq,Array.append
(Array.map (fun x->lift lifti x) a) eqa)
with Not_found -> raise(EqNotFound (ind',ind))
@@ -233,7 +233,7 @@ let build_beq_scheme kn =
let ar2 = Array.create n ff in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
- if (i=j) then
+ if Int.equal i j then
ar2.(j) <- let cc = (match nb_cstr_args with
| 0 -> tt
| _ -> let eqs = Array.make nb_cstr_args tt in
@@ -319,7 +319,7 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
let s = destVar v in
let n = Array.length avoid in
let rec find i =
- if avoid.(n-i) = s then avoid.(n-i-x)
+ if id_eq avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
else error ("Var "^(string_of_id s)^" seems unknown.")
)
@@ -329,7 +329,7 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
(
let mp,dir,lbl = repr_con (destConst v) in
mkConst (make_con mp dir (mk_label (
- if offset=1 then ("eq_"^(string_of_label lbl))
+ if Int.equal offset 1 then ("eq_"^(string_of_label lbl))
else ((string_of_label lbl)^"_lb")
)))
)
@@ -353,7 +353,7 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
(Array.map (fun x -> x) v)
(Array.map (fun x -> do_arg x 1) v))
(Array.map (fun x -> do_arg x 2) v)
- in let app = if lb_args = [||]
+ in let app = if Array.equal eq_constr lb_args [||]
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in [Equality.replace p q ; apply app ; Auto.default_auto]
@@ -366,7 +366,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
let s = destVar v in
let n = Array.length avoid in
let rec find i =
- if avoid.(n-i) = s then avoid.(n-i-x)
+ if id_eq avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
else error ("Var "^(string_of_id s)^" seems unknown.")
)
@@ -376,7 +376,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
(
let mp,dir,lbl = repr_con (destConst v) in
mkConst (make_con mp dir (mk_label (
- if offset=1 then ("eq_"^(string_of_label lbl))
+ if Int.equal offset 1 then ("eq_"^(string_of_label lbl))
else ((string_of_label lbl)^"_bl")
)))
)
@@ -385,12 +385,12 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in
- if t1=t2 then aux q1 q2
+ if eq_constr t1 t2 then aux q1 q2
else (
let u,v = try destruct_ind tt1
(* trick so that the good sequence is returned*)
with _ -> ind,[||]
- in if u = ind
+ in if eq_ind u ind
then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
else (
let bl_t1 =
@@ -412,7 +412,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
(Array.map (fun x -> do_arg x 1) v))
(Array.map (fun x -> do_arg x 2) v )
in
- let app = if bl_args = [||]
+ let app = if Array.equal eq_constr bl_args [||]
then bl_t1 else mkApp (bl_t1,bl_args)
in
(Equality.replace_by t1 t2
@@ -434,7 +434,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
_ -> (try fst (destConstruct ind2) with _ ->
error "The expected type is an inductive one.")
in
- if (sp1 <> sp2) || (i1 <> i2)
+ if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
then (error "Eq should be on the same type")
else (aux (Array.to_list ca1) (Array.to_list ca2))
@@ -461,7 +461,7 @@ let eqI ind l =
and e = try mkConst (find_scheme beq_scheme_kind ind) with
Not_found -> error
("The boolean equality on "^(string_of_mind (fst ind))^" is needed.");
- in (if eA = [||] then e else mkApp(e,eA))
+ in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA))
(**********************************************************************)
(* Boolean->Leibniz *)
@@ -558,7 +558,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
| App (c,ca) -> (
match (kind_of_term c) with
| Ind indeq ->
- if IndRef indeq = Coqlib.glob_eq
+ if eq_gr (IndRef indeq) Coqlib.glob_eq
then (
tclTHENSEQ ((do_replace_bl bl_scheme_key ind gls
(!avoid)
@@ -577,7 +577,7 @@ let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
let make_bl_scheme mind =
let mib = Global.lookup_mind mind in
- if Array.length mib.mind_packets <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) then
errorlabstrm ""
(str "Automatic building of boolean->Leibniz lemmas not supported");
let ind = (mind,0) in
@@ -689,7 +689,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
let make_lb_scheme mind =
let mib = Global.lookup_mind mind in
- if Array.length mib.mind_packets <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) then
errorlabstrm ""
(str "Automatic building of Leibniz->boolean lemmas not supported");
let ind = (mind,0) in
@@ -844,7 +844,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
let make_eq_decidability mind =
let mib = Global.lookup_mind mind in
- if Array.length mib.mind_packets <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) then
anomaly "Decidability lemma for mutual inductive types not supported";
let ind = (mind,0) in
let nparams = mib.mind_nparams in
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 2338e7f39..0c0ee38e6 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -7,6 +7,7 @@
(************************************************************************)
(*i*)
+open Util
open Pp
open Printer
open Names
@@ -33,7 +34,7 @@ type instance_decl_function = global_reference -> rel_context -> constr list ->
let rec subst_evar evar def n c =
match kind_of_term c with
- | Evar (e,_) when e=evar -> lift n def
+ | Evar (e,_) when Int.equal e evar -> lift n def
| _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c
let subst_evar_in_evm evar def evm =
@@ -57,7 +58,7 @@ let rec safe_define evm ev c =
let define_subst evm sigma =
Util.Intmap.fold
( fun ev (e,c) evm ->
- match kind_of_term c with Evar (i,_) when i=ev -> evm | _ ->
+ match kind_of_term c with Evar (i,_) when Int.equal i ev -> evm | _ ->
safe_define evm ev (lift (-List.length e) c)
) sigma evm in
match evi.evar_body with
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 4e4b2135d..37496387e 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Names
open Vernacexpr
@@ -157,10 +158,10 @@ let back count =
Return the final state number. *)
let backto snum =
- if snum = Lib.current_command_label () then snum
+ if Int.equal snum (Lib.current_command_label ()) then snum
else
let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
- search (fun i -> i.label = snum);
+ search (fun i -> Int.equal i.label snum);
fst (sync nb_opened_proofs)
(** Old [Backtrack] code with corresponding update of the history stack.
@@ -172,7 +173,7 @@ let backto snum =
let backtrack snum pnum naborts =
raw_backtrack snum pnum naborts;
- search (fun i -> i.label = snum)
+ search (fun i -> Int.equal i.label snum)
(** [reset_initial] resets the system and clears the command history
stack, only pushing back the initial entry. It should be equivalent
@@ -180,7 +181,7 @@ let backtrack snum pnum naborts =
let reset_initial () =
let init_label = Lib.first_command_label in
- if Lib.current_command_label () = init_label then ()
+ if Int.equal (Lib.current_command_label ()) init_label then ()
else begin
Pfedit.delete_all_proofs ();
Lib.reset_label init_label;
@@ -227,7 +228,7 @@ let get_script prf =
let script = ref [] in
let select i = match i.prfname with
| None -> raise Not_found
- | Some p when p=prf && i.reachable -> script := i :: !script
+ | Some p when id_eq p prf && i.reachable -> script := i :: !script
| _ -> ()
in
(try Stack.iter select history with Not_found -> ());
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0696299b3..9a9c99c12 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Pp
open Errors
open Indtypes
@@ -14,7 +15,7 @@ open Pretype_errors
open Indrec
let print_loc loc =
- if loc = Loc.ghost then
+ if Loc.is_ghost loc then
(str"<unknown>")
else
let loc = Loc.unloc loc in
@@ -41,12 +42,12 @@ let explain_exn_default = function
| Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
(* Meta-exceptions *)
| Loc.Exc_located (loc,exc) ->
- hov 0 ((if loc = Loc.ghost then (mt ())
+ hov 0 ((if Loc.is_ghost loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ Errors.print_no_anomaly exc)
| Compat.Exc_located (loc, exc) ->
let loc = Compat.to_coqloc loc in
- hov 0 ((if loc = Loc.ghost then (mt ())
+ hov 0 ((if Loc.is_ghost loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ Errors.print_no_anomaly exc)
| EvaluatedError (msg,None) -> msg
@@ -62,6 +63,9 @@ let _ = Errors.register_handler explain_exn_default
let wrap_vernac_error strm =
EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
+let is_mt t =
+ Pervasives.(=) (Lazy.force t) (mt ()) (* FIXME *)
+
let rec process_vernac_interp_error = function
| Univ.UniverseInconsistency (o,u,v,p) ->
let pr_rel r =
@@ -73,7 +77,7 @@ let rec process_vernac_interp_error = function
str " because" ++ spc() ++ Univ.pr_uni v ++
prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ Univ.pr_uni v)
p ++
- (if snd (CList.last p)=u then mt() else
+ (if Pervasives.(=) (snd (List.last p)) u then mt() else (* FIXME *)
(spc() ++ str "= " ++ Univ.pr_uni u)) in
let msg =
if !Constrextern.print_universes then
@@ -114,11 +118,11 @@ let rec process_vernac_interp_error = function
| Refiner.FailError (i,s) ->
wrap_vernac_error
(str "Tactic failure" ++
- (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
- if i=0 then str "." else str " (level " ++ int i ++ str").")
+ (if not (is_mt s) then str ":" ++ Lazy.force s else mt ()) ++ (* FIXME *)
+ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
| AlreadyDeclared msg ->
wrap_vernac_error (msg ++ str ".")
- | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
+ | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
process_vernac_interp_error exc
| Proof_type.LtacLocated (s,exc) ->
EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 87310302c..aa77a00c5 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -76,7 +76,7 @@ let check_arity = function
(* check that the computed target is the provided one *)
let check_target clt = function
- | Some cl when cl <> clt -> raise (CoercionError (WrongTarget(clt,cl)))
+ | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl)))
| _ -> ()
(* condition d'heritage uniforme *)
@@ -86,7 +86,7 @@ let uniform_cond nargs lt =
| (0,[]) -> true
| (n,t::l) ->
let t = strip_outer_cast t in
- isRel t && destRel t = n && aux ((n-1),l)
+ isRel t && Int.equal (destRel t) n && aux ((n-1),l)
| _ -> false
in
aux (nargs,lt)
@@ -127,7 +127,7 @@ let get_source lp source =
| t1::lt ->
try
let cl1,lv1 = find_class_type Evd.empty t1 in
- if cl = cl1 then cl1,lv1,(List.length lt+1)
+ if cl_typ_eq cl cl1 then cl1,lv1,(List.length lt+1)
else raise Not_found
with Not_found -> aux lt
in aux (List.rev lp)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 38b5703f3..43caf3fa3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -194,7 +194,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
let subst =
match props with
- | None -> if k.cl_props = [] then Some (Inl subst) else None
+ | None -> if List.is_empty k.cl_props then Some (Inl subst) else None
| Some (Inr term) ->
let c = interp_casted_constr_evars evars env' term cty in
Some (Inr (c, subst))
@@ -207,17 +207,21 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let props, rest =
List.fold_left
(fun (props, rest) (id,b,_) ->
- if b = None then
+ if Option.is_empty b then
try
- let (loc_mid, c) =
- List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest
+ let is_id (id', _) = match id, get_id id' with
+ | Name id, (_, id') -> id_eq id id'
+ | Anonymous, _ -> false
+ in
+ let (loc_mid, c) =
+ List.find is_id rest
in
let rest' =
- List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest
+ List.filter (fun v -> not (is_id v)) rest
in
let (loc, mid) = get_id loc_mid in
List.iter (fun (n, _, x) ->
- if n = Name mid then
+ if name_eq n (Name mid) then
Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
k.cl_projs;
c :: props, rest'
@@ -226,9 +230,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
else props, rest)
([], props) k.cl_props
in
- if rest <> [] then
- unbound_method env' k.cl_impl (get_id (fst (List.hd rest)))
- else
+ match rest with
+ | (n, _) :: _ ->
+ unbound_method env' k.cl_impl (get_id n)
+ | _ ->
Some (Inl (type_ctx_instance evars (push_rel_context ctx' env')
k.cl_props props subst))
in
@@ -238,7 +243,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
None, termtype
| Some (Inl subst) ->
let subst = List.fold_left2
- (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+ (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
let app, ty_constr = instance_constructor k subst in
@@ -265,7 +270,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let term = Option.map (Evarutil.nf_evar !evars) term in
let evm = Evarutil.nf_evar_map_undefined !evars in
let evm = undefined_evars evm in
- if Evd.is_empty evm && term <> None then
+ if Evd.is_empty evm && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
else begin
let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -291,7 +296,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
(fun () ->
Lemmas.start_proof id kind termtype
(fun _ -> instance_hook k pri global imps ?hook);
- if term <> None then
+ if not (Option.is_empty term) then
Pfedit.by (!refine_ref (evm, Option.get term))
else if Flags.is_auto_intros () then
Pfedit.by (Refiner.tclDO len Tactics.intro);
@@ -333,7 +338,7 @@ let context l =
else (
let impl = List.exists
(fun (x,_) ->
- match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+ match x with ExplByPos (_, Some id') -> id_eq id id' | _ -> false) impls
in
Command.declare_assumption false (Local (* global *), Definitional) t
[] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f707ea508..5967b435a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -88,8 +88,10 @@ let interp_definition bl red_option c ctypopt =
let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in
let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
+ let beq b1 b2 = if b1 then b2 else not b2 in
+ let impl_eq (x1, y1, z1) (x2, y2, z2) = beq x1 x2 && beq y1 y2 && beq z1 z2 in
(* Check that all implicit arguments inferable from the term is inferable from the type *)
- if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false)
+ if not (try List.for_all (fun (key,va) -> impl_eq (List.assoc key impsty) va) imps2 with Not_found -> false)
then msg_warning (strbrk "Implicit arguments declaration relies on type." ++
spc () ++ strbrk "The term declares more implicits than the type here.");
imps1@(Impargs.lift_implicits nb_args impsty),
@@ -110,7 +112,7 @@ let declare_global_definition ident ce local k imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in
let gr = ConstRef kn in
maybe_declare_manual_implicits false gr imps;
- if local = Local && Flags.is_verbose() then
+ if local == Local && Flags.is_verbose() then
msg_warning (pr_id ident ++ strbrk " is declared as a global definition");
definition_message ident;
Autoinstance.search_declaration (ConstRef kn);
@@ -165,7 +167,7 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
declare_variable ident
(Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
assumption_message ident;
- if is_verbose () & Pfedit.refining () then
+ if is_verbose () && Pfedit.refining () then
msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
strbrk " is not visible from current goals");
let r = VarRef ident in
@@ -177,7 +179,7 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
let gr = ConstRef kn in
maybe_declare_manual_implicits false gr imps;
assumption_message ident;
- if local=Local & Flags.is_verbose () then
+ if local == Local && Flags.is_verbose () then
msg_warning (pr_id ident ++ strbrk " is declared as a parameter" ++
strbrk " because it is at a global level");
Autoinstance.search_declaration (ConstRef kn);
@@ -226,11 +228,19 @@ let check_all_names_different indl =
let ind_names = List.map (fun ind -> ind.ind_name) indl in
let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
let l = List.duplicates ind_names in
- if l <> [] then raise (InductiveError (SameNamesTypes (List.hd l)));
+ let () = match l with
+ | [] -> ()
+ | t :: _ -> raise (InductiveError (SameNamesTypes t))
+ in
let l = List.duplicates cstr_names in
- if l <> [] then raise (InductiveError (SameNamesConstructors (List.hd l)));
+ let () = match l with
+ | [] -> ()
+ | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l)))
+ in
let l = List.intersect ind_names cstr_names in
- if l <> [] then raise (InductiveError (SameNamesOverlap l))
+ match l with
+ | [] -> ()
+ | _ -> raise (InductiveError (SameNamesOverlap l))
let mk_mltype_data evdref env assums arity indname =
let is_ml_type = is_sort env !evdref arity in
@@ -261,7 +271,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* Names of parameters as arguments of the inductive type (defs removed) *)
- let assums = List.filter(fun (_,b,_) -> b=None) ctx_params in
+ let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
let params = List.map (fun (na,_,_) -> out_name na) assums in
(* Interpret the arities *)
@@ -320,16 +330,16 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Very syntactical equality *)
let eq_local_binder d1 d2 = match d1,d2 with
| LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
- List.length nal1 = List.length nal2 && k1 = k2 &&
- List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
+ Int.equal (List.length nal1) (List.length nal2) && binder_kind_eq k1 k2 &&
+ List.for_all2 (fun (_,na1) (_,na2) -> name_eq na1 na2) nal1 nal2 &&
Constrextern.is_same_type c1 c2
| LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
- id1 = id2 && Constrextern.is_same_type c1 c2
+ name_eq id1 id2 && Constrextern.is_same_type c1 c2
| _ ->
false
let eq_local_binders bl1 bl2 =
- List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2
+ Int.equal (List.length bl1) (List.length bl2) && List.for_all2 eq_local_binder bl1 bl2
let extract_coercions indl =
let mkqid (_,((_,id),_)) = qualid_of_ident id in
@@ -430,7 +440,7 @@ let rec partial_order = function
let res = List.remove_assoc y res in
let res = List.map (function
| (z, Inl t) ->
- if t = y then (z, Inl x) else (z, Inl t)
+ if id_eq t y then (z, Inl x) else (z, Inl t)
| (z, Inr zge) ->
if List.mem y zge then
(z, Inr (List.add_set x (List.remove y zge)))
@@ -451,7 +461,7 @@ let non_full_mutual_message x xge y yge isfix rest =
string_of_id x^" depends on "^string_of_id y^" but not conversely"
else
string_of_id y^" and "^string_of_id x^" are not mutually dependent" in
- let e = if rest <> [] then "e.g.: "^reason else reason in
+ let e = if List.is_empty rest then reason else "e.g.: "^reason in
let k = if isfix then "fixpoint" else "cofixpoint" in
let w =
if isfix
@@ -464,7 +474,7 @@ let check_mutuality env isfix fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
- (id, List.filter (fun id' -> id<>id' & occur_var env id' def) names))
+ (id, List.filter (fun id' -> not (id_eq id id') && occur_var env id' def) names))
fixl in
let po = partial_order preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -700,7 +710,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
in
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
- if Impargs.is_implicit_args () || impls <> [] then
+ if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in
let typ = it_mkProd_or_LetIn top_arity binders in
@@ -708,7 +718,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
else
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook l gr =
- if Impargs.is_implicit_args () || impls <> [] then
+ if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
@@ -862,7 +872,7 @@ let collect_evars_of_term evd c ty =
evars Evd.empty
let do_program_recursive fixkind fixl ntns =
- let isfix = fixkind <> Obligations.IsCoFixpoint in
+ let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, evd), fix, info =
interp_recursive isfix fixl ntns
in
@@ -916,7 +926,7 @@ let do_program_fixpoint l =
build_wellfounded (id, n, bl, typ, out_def def)
(Option.default (CRef lt_ref) r) m ntn
- | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
+ | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
let fixl,ntns = extract_fixpoint_components true l in
let fixkind = Obligations.IsFixpoint g in
do_program_recursive fixkind fixl ntns
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 718e65b50..3b5034e95 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Pp
let (/) = Filename.concat
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e8e924d52..b196e6b4b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -55,7 +55,7 @@ let set_batch_mode () = batch_mode := true
let toplevel_default_name = make_dirpath [id_of_string "Top"]
let toplevel_name = ref (Some toplevel_default_name)
let set_toplevel_name dir =
- if dir = empty_dirpath then error "Need a non empty toplevel module name";
+ if dir_path_eq dir empty_dirpath then error "Need a non empty toplevel module name";
toplevel_name := Some dir
let unset_toplevel_name () = toplevel_name := None
@@ -63,11 +63,11 @@ let remove_top_ml () = Mltop.remove ()
let inputstate = ref ""
let set_inputstate s = inputstate:=s
-let inputstate () = if !inputstate <> "" then intern_state !inputstate
+let inputstate () = if not (String.equal !inputstate "") then intern_state !inputstate
let outputstate = ref ""
let set_outputstate s = outputstate:=s
-let outputstate () = if !outputstate <> "" then extern_state !outputstate
+let outputstate () = if not (String.equal !outputstate "") then extern_state !outputstate
let set_default_include d = push_include (d,Nameops.default_root_prefix)
let set_include d p =
@@ -184,8 +184,8 @@ let parse_args arglist =
let rec parse = function
| [] -> []
| "-with-geoproof" :: s :: rem ->
- if s = "yes" then Coq_config.with_geoproof := true
- else if s = "no" then Coq_config.with_geoproof := false
+ if String.equal s "yes" then Coq_config.with_geoproof := true
+ else if String.equal s "no" then Coq_config.with_geoproof := false
else usage ();
parse rem
| "-impredicative-set" :: rem ->
@@ -370,7 +370,7 @@ let init arglist =
(* Be careful to set these variables after the inputstate *)
Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
Syntax_def.set_compat_notations (not !no_compat_ntn);
- if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
+ if (not !batch_mode|| List.is_empty !compile_list) && Global.env_is_empty() then
Option.iter Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ac86a04b9..2f2040199 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -332,8 +332,8 @@ let explain_occur_check env sigma ev rhs =
pt ++ spc () ++ str "that would depend on itself."
let pr_ne_context_of header footer env =
- if Environ.rel_context env = empty_rel_context &
- Environ.named_context env = empty_named_context
+ if List.is_empty (Environ.rel_context env) &&
+ List.is_empty (Environ.named_context env)
then footer
else pr_ne_context_of header env
@@ -404,7 +404,7 @@ let explain_var_not_found env id =
let explain_wrong_case_info env ind ci =
let pi = pr_inductive (Global.env()) ind in
- if ci.ci_ind = ind then
+ if eq_ind ci.ci_ind ind then
str "Pattern-matching expression on an object of inductive type" ++
spc () ++ pi ++ spc () ++ str "has invalid information."
else
@@ -700,7 +700,7 @@ let is_goal_evar evi = match evi.evar_source with (_, Evar_kinds.GoalEvar) -> tr
let pr_constraints printenv env evm =
let l = Evd.to_list evm in
- assert(l <> []);
+ assert(not (List.is_empty l));
let (ev, evi) = List.hd l in
if List.for_all (fun (ev', evi') ->
eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
@@ -816,12 +816,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
pv ++
(* warning: because of implicit arguments it is difficult to say which
parameters must be explicitly given *)
- (if nparams<>0 then
+ (if not (Int.equal nparams 0) then
strbrk " applied to its " ++ str (String.plural nparams "parameter")
else
mt()) ++
- (if nargs<>0 then
- str (if nparams<>0 then " and" else " applied") ++
+ (if not (Int.equal nargs 0) then
+ str (if not (Int.equal nparams 0) then " and" else " applied") ++
strbrk " to some " ++ str (String.plural nargs "argument")
else
mt()) ++ str "."
@@ -868,7 +868,7 @@ let error_not_allowed_case_analysis isrec kind i =
pr_inductive (Global.env()) i ++ str "."
let error_not_mutual_in_scheme ind ind' =
- if ind = ind' then
+ if eq_ind ind ind' then
str "The inductive type " ++ pr_inductive (Global.env()) ind ++
str " occurs twice."
else
@@ -1013,7 +1013,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
let unboundvars = List.map_filter filter unboundvars in
quote (pr_glob_constr_env (Global.env()) c) ++
- (if unboundvars <> [] or vars <> [] then
+ (if not (List.is_empty unboundvars) || not (List.is_empty vars) then
strbrk " (with " ++
prlist_with_sep pr_comma
(fun (id,c) ->
@@ -1023,7 +1023,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
(if Int.equal n 2 then str " (repeated twice)"
else if n>2 then str " (repeated "++int n++str" times)"
else mt()) in
- if calls <> [] then
+ if not (List.is_empty calls) then
let kind_of_last_call = match List.last calls with
| (_,Proof_type.LtacConstrInterp _) -> ", last term evaluation failed."
| _ -> ", last call failed." in
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 43f9761c0..c12bbae7a 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -288,11 +288,11 @@ let eval_call c =
| Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
| Error_in_file (_,_,inner) -> None, pr_exn inner
| Loc.Exc_located (loc, inner) ->
- let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in
+ let loc = if Loc.is_ghost loc then None else Some (Loc.unloc loc) in
loc, pr_exn inner
| Compat.Exc_located (loc, inner) ->
let loc = Compat.to_coqloc loc in
- let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in
+ let loc = if Loc.is_ghost loc then None else Some (Loc.unloc loc) in
loc, pr_exn inner
| e -> None, pr_exn e
in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index bfd64778f..44b87b0c6 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -89,7 +89,7 @@ let scheme_object_table =
let declare_scheme_object s aux f =
(try check_ident ("ind"^s) with _ ->
error ("Illegal induction scheme suffix: "^s));
- let key = if aux = "" then s else aux in
+ let key = if String.equal aux "" then s else aux in
try
let _ = Hashtbl.find scheme_object_table key in
(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index b3ea8438a..2f01e7323 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -193,7 +193,7 @@ let declare_beq_scheme = declare_beq_scheme_with []
let declare_one_case_analysis_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
- let dep = if kind = InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+ let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
let kelim = elim_sorts (mib,mip) in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
@@ -216,7 +216,7 @@ let kinds_from_type =
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
- let from_prop = kind = InProp in
+ let from_prop = kind == InProp in
let kelim = elim_sorts (mib,mip) in
let elims =
List.map_filter (fun (sort,kind) ->
@@ -361,7 +361,7 @@ let do_mutual_induction_scheme lnamedepindsort =
let get_common_underlying_mutual_inductive = function
| [] -> assert false
| (id,(mind,i as ind))::l as all ->
- match List.filter (fun (_,(mind',_)) -> mind <> mind') l with
+ match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
| (_,ind')::_ ->
raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
| [] ->
@@ -375,11 +375,11 @@ let do_scheme l =
let ischeme,escheme = split_scheme l in
(* we want 1 kind of scheme at a time so we check if the user
tried to declare different schemes at once *)
- if (ischeme <> []) && (escheme <> [])
+ if not (List.is_empty ischeme) && not (List.is_empty escheme)
then
error "Do not declare equality and induction scheme at the same time."
else (
- if ischeme <> [] then do_mutual_induction_scheme ischeme
+ if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
else
let mind,l = get_common_underlying_mutual_inductive escheme in
declare_beq_scheme_with l mind;
@@ -392,7 +392,7 @@ tried to declare different schemes at once *)
let list_split_rev_at index l =
let rec aux i acc = function
- hd :: tl when i = index -> acc, tl
+ hd :: tl when Int.equal i index -> acc, tl
| hd :: tl -> aux (succ i) (hd :: acc) tl
| [] -> failwith "List.split_when: Invalid argument"
in aux 0 [] l
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index a49305292..ecd1cc59b 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -71,7 +71,7 @@ let find_mutually_recursive_statements thms =
(match kind_of_term t with
| Ind (kn,_ as ind) when
let mind = Global.lookup_mind kn in
- mind.mind_finite & b = None ->
+ mind.mind_finite && Option.is_empty b ->
[ind,x,i],[]
| _ ->
error "Decreasing argument is not an inductive assumption.")
@@ -88,7 +88,7 @@ let find_mutually_recursive_statements thms =
match kind_of_term t with
| Ind (kn,_ as ind) when
let mind = Global.lookup_mind kn in
- mind.mind_finite & b = None ->
+ mind.mind_finite && Option.is_empty b ->
[ind,x,i]
| _ ->
[]) 0 (List.rev whnf_hyp_hds)) in
@@ -98,13 +98,13 @@ let find_mutually_recursive_statements thms =
match kind_of_term whnf_ccl with
| Ind (kn,_ as ind) when
let mind = Global.lookup_mind kn in
- mind.mind_ntypes = n & not mind.mind_finite ->
+ Int.equal mind.mind_ntypes n && not mind.mind_finite ->
[ind,x,0]
| _ ->
[] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
(* Check if all conclusions are coinductive in the same type *)
(* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
@@ -112,7 +112,7 @@ let find_mutually_recursive_statements thms =
if List.for_all (of_same_mutind hyp) oks
then Some (hyp::oks) else None) [] ind_ccls in
let ordered_same_indccl =
- List.filter (List.for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
+ List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
(* Check if some hypotheses are inductive in the same type *)
let common_same_indhyp =
List.cartesians_filter (fun hyp oks ->
@@ -121,16 +121,19 @@ let find_mutually_recursive_statements thms =
let ordered_inds,finite,guard =
match ordered_same_indccl, common_same_indhyp with
| indccl::rest, _ ->
- assert (rest=[]);
+ assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
- if common_same_indhyp <> [] then
+ if not (List.is_empty common_same_indhyp) then
if_verbose msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
- if same_indccl <> [] &&
- List.distinct (List.map pi1 (List.hd same_indccl)) then
- if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
+ let () = match same_indccl with
+ | ind :: _ ->
+ if List.distinct (List.map pi1 ind) then
+ if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ()
+ | _ -> ()
+ in
let possible_guards = List.map (List.map pi3) inds_hyps in
(* assume the largest indices as possible *)
List.last common_same_indhyp, false, possible_guards
@@ -180,7 +183,7 @@ let compute_proof_name locality = function
| Some (loc,id) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
- locality=Global && Nametab.exists_cci (Lib.make_path_except_section id)
+ locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err_loc (loc,"",pr_id id ++ str " already exists.");
id
@@ -233,7 +236,7 @@ let save_named opacity =
save id const do_guard persistence hook
let check_anonymity id save_ident =
- if atompart_of_id id <> string_of_id (default_thm_id) then
+ if not (String.equal (atompart_of_id id) (string_of_id (default_thm_id))) then
error "This command can only be used for unnamed theorem."
let save_anonymous opacity save_ident =
@@ -299,7 +302,7 @@ let start_proof_with_initialization kind recguard thms snl hook =
| (id,(t,(_,imps)))::other_thms ->
let hook strength ref =
let other_thms_data =
- if other_thms = [] then [] else
+ if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
let body,opaq = retrieve_first_recthm ref in
List.map_i (save_remaining_recthms kind body opaq) 1 other_thms in
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c3ca35fe5..17bae5f9e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -185,16 +185,16 @@ let parse_format ((loc, str) : lstring) =
| a::(_::_ as l) -> push_token (UnpBox (b,a)) l
| _ -> error "Non terminated box in format." in
let close_quotation i =
- if i < String.length str & str.[i] = '\'' & (i+1 = l or str.[i+1] = ' ')
+ if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
then i+1
else error "Incorrectly terminated quoted expression." in
let rec spaces n i =
- if i < String.length str & str.[i] = ' ' then spaces (n+1) (i+1)
+ if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
else n in
let rec nonspaces quoted n i =
- if i < String.length str & str.[i] <> ' ' then
- if str.[i] = '\'' & quoted &
- (i+1 >= String.length str or str.[i+1] = ' ')
+ if i < String.length str && str.[i] != ' ' then
+ if str.[i] == '\'' && quoted &&
+ (i+1 >= String.length str || str.[i+1] == ' ')
then if Int.equal n 0 then error "Empty quoted token." else n
else nonspaces quoted (n+1) (i+1)
else
@@ -206,7 +206,7 @@ let parse_format ((loc, str) : lstring) =
and parse_quoted n i =
if i < String.length str then match str.[i] with
(* Parse " // " *)
- | '/' when i <= String.length str & str.[i+1] = '/' ->
+ | '/' when i <= String.length str && str.[i+1] == '/' ->
(* We forget the useless n spaces... *)
push_token (UnpCut PpFnl)
(parse_token (close_quotation (i+2)))
@@ -221,7 +221,7 @@ let parse_format ((loc, str) : lstring) =
| '[' ->
if i <= String.length str then match str.[i+1] with
(* Parse " [h .. ", *)
- | 'h' when i+1 <= String.length str & str.[i+2] = 'v' ->
+ | 'h' when i+1 <= String.length str && str.[i+2] == 'v' ->
(parse_box (fun n -> PpHVB n) (i+3))
(* Parse " [v .. ", *)
| 'v' ->
@@ -250,7 +250,7 @@ let parse_format ((loc, str) : lstring) =
let i = i+n in
if i < l then match str.[i] with
(* Parse a ' *)
- | '\'' when i+1 >= String.length str or str.[i+1] = ' ' ->
+ | '\'' when i+1 >= String.length str || str.[i+1] == ' ' ->
push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1)))
(* Parse the beginning of a quoted expression *)
| '\'' ->
@@ -261,7 +261,7 @@ let parse_format ((loc, str) : lstring) =
else push_white n [[]]
in
try
- if str <> "" then match parse_token 0 with
+ if not (String.equal str "") then match parse_token 0 with
| [l] -> l
| _ -> error "Box closed without being opened in format."
else
@@ -276,16 +276,16 @@ type symbol_token = WhiteSpace of int | String of string
let split_notation_string str =
let push_token beg i l =
- if beg = i then l else
+ if Int.equal beg i then l else
let s = String.sub str beg (i - beg) in
String s :: l
in
let push_whitespace beg i l =
- if beg = i then l else WhiteSpace (i-beg) :: l
+ if Int.equal beg i then l else WhiteSpace (i-beg) :: l
in
let rec loop beg i =
if i < String.length str then
- if str.[i] = ' ' then
+ if str.[i] == ' ' then
push_token beg i (loop_on_whitespace (i+1) (i+1))
else
loop beg (i+1)
@@ -293,7 +293,7 @@ let split_notation_string str =
push_token beg i []
and loop_on_whitespace beg i =
if i < String.length str then
- if str.[i] <> ' ' then
+ if str.[i] != ' ' then
push_whitespace beg i (loop i (i+1))
else
loop_on_whitespace beg (i+1)
@@ -307,9 +307,9 @@ let split_notation_string str =
let out_nt = function NonTerminal x -> x | _ -> assert false
let rec find_pattern nt xl = function
- | Break n as x :: l, Break n' :: l' when n=n' ->
+ | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
find_pattern nt (x::xl) (l,l')
- | Terminal s as x :: l, Terminal s' :: l' when s = s' ->
+ | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
find_pattern nt (x::xl) (l,l')
| [], NonTerminal x' :: l' ->
(out_nt nt,x',List.rev xl),l'
@@ -324,7 +324,7 @@ let rec find_pattern nt xl = function
let rec interp_list_parser hd = function
| [] -> [], List.rev hd
- | NonTerminal id :: tl when id = ldots_var ->
+ | NonTerminal id :: tl when id_eq id ldots_var ->
let hd = List.rev hd in
let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
let xyl,tl'' = interp_list_parser [] tl' in
@@ -332,7 +332,7 @@ let rec interp_list_parser hd = function
(* remove the second copy of it afterwards *)
(x,y)::xyl, SProdList (x,sl) :: tl''
| (Terminal _ | Break _) as s :: tl ->
- if hd = [] then
+ if List.is_empty hd then
let yl,tl' = interp_list_parser [] tl in
yl, s :: tl'
else
@@ -349,7 +349,7 @@ let rec interp_list_parser hd = function
let quote_notation_token x =
let n = String.length x in
let norm = Lexer.is_ident x in
- if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
+ if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
else x
let rec raw_analyze_notation_tokens = function
@@ -374,7 +374,7 @@ let rec get_notation_vars = function
| [] -> []
| NonTerminal id :: sl ->
let vars = get_notation_vars sl in
- if id = ldots_var then vars else
+ if id_eq id ldots_var then vars else
if List.mem id vars then
error ("Variable "^string_of_id id^" occurs more than once.")
else
@@ -406,7 +406,7 @@ let prec_assoc = function
let precedence_of_entry_type from = function
| ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n
| ETConstr (NumLevel n,BorderProd (b,Some a)) ->
- n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp
+ n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
| ETConstr (NumLevel n,InternalProd) -> n, Prec n
| ETConstr (NextLevel,_) -> from, L
| _ -> 0, E (* ?? *)
@@ -420,25 +420,25 @@ let precedence_of_entry_type from = function
(* "< x , y > { z , t }" : "< x , / y > / { z , / t }" *)
let is_left_bracket s =
- let l = String.length s in l <> 0 &
- (s.[0] = '{' or s.[0] = '[' or s.[0] = '(')
+ let l = String.length s in not (Int.equal l 0) &&
+ (s.[0] == '{' || s.[0] == '[' || s.[0] == '(')
let is_right_bracket s =
- let l = String.length s in l <> 0 &
- (s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')')
+ let l = String.length s in not (Int.equal l 0) &&
+ (s.[l-1] == '}' || s.[l-1] == ']' || s.[l-1] == ')')
let is_comma s =
- let l = String.length s in l <> 0 &
- (s.[0] = ',' or s.[0] = ';')
+ let l = String.length s in not (Int.equal l 0) &&
+ (s.[0] == ',' || s.[0] == ';')
let is_operator s =
- let l = String.length s in l <> 0 &
- (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or
- s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
- s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$')
+ let l = String.length s in not (Int.equal l 0) &&
+ (s.[0] == '+' || s.[0] == '*' || s.[0] == '=' ||
+ s.[0] == '-' || s.[0] == '/' || s.[0] == '<' || s.[0] == '>' ||
+ s.[0] == '@' || s.[0] == '\\' || s.[0] == '&' || s.[0] == '~' || s.[0] == '$')
let is_prod_ident = function
- | Terminal s when is_letter s.[0] or s.[0] = '_' -> true
+ | Terminal s when is_letter s.[0] || s.[0] == '_' -> true
| _ -> false
let is_non_terminal = function
@@ -448,7 +448,7 @@ let is_non_terminal = function
let add_break n l = UnpCut (PpBrk(n,0)) :: l
let check_open_binder isopen sl m =
- if isopen & sl <> [] then
+ if isopen && not (List.is_empty sl) then
errorlabstrm "" (str "as " ++ pr_id m ++
str " is a non-closed binder, no such \"" ++
prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
@@ -465,33 +465,34 @@ let make_hunks etyps symbols from =
let i = List.index m vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
let u = UnpMetaVar (i,prec) in
- if prods <> [] && is_non_terminal (List.hd prods) then
+ begin match prods with
+ | s :: _ when is_non_terminal s ->
u :: add_break 1 (make CanBreak prods)
- else
+ | _ ->
u :: make CanBreak prods
-
+ end
| Terminal s :: prods when List.exists is_non_terminal prods ->
if is_comma s then
UnpTerminal s :: add_break 1 (make NoBreak prods)
else if is_right_bracket s then
UnpTerminal s :: add_break 0 (make NoBreak prods)
else if is_left_bracket s then
- if ws = CanBreak then
+ if ws == CanBreak then
add_break 1 (UnpTerminal s :: make CanBreak prods)
else
UnpTerminal s :: make CanBreak prods
else if is_operator s then
- if ws = CanBreak then
+ if ws == CanBreak then
UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods)
else
UnpTerminal s :: add_break 1 (make NoBreak prods)
else if is_ident_tail s.[String.length s - 1] then
let sep = if is_prod_ident (List.hd prods) then "" else " " in
- if ws = CanBreak then
+ if ws == CanBreak then
add_break 1 (UnpTerminal (s^sep) :: make CanBreak prods)
else
UnpTerminal (s^sep) :: make CanBreak prods
- else if ws = CanBreak then
+ else if ws == CanBreak then
add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
else
UnpTerminal s :: make CanBreak prods
@@ -499,7 +500,7 @@ let make_hunks etyps symbols from =
| Terminal s :: prods ->
if is_right_bracket s then
UnpTerminal s :: make NoBreak prods
- else if ws = CanBreak then
+ else if ws == CanBreak then
add_break 1 (UnpTerminal s :: make NoBreak prods)
else
UnpTerminal s :: make NoBreak prods
@@ -513,7 +514,7 @@ let make_hunks etyps symbols from =
let _,prec = precedence_of_entry_type from typ in
let sl' =
(* If no separator: add a break *)
- if sl = [] then add_break 1 []
+ if List.is_empty sl then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
else snd (List.sep_last (make NoBreak (sl@[NonTerminal m]))) in
let hunk = match typ with
@@ -533,7 +534,7 @@ let make_hunks etyps symbols from =
let error_format () = error "The format does not match the notation."
let rec split_format_at_ldots hd = function
- | UnpTerminal s :: fmt when s = string_of_id ldots_var -> List.rev hd, fmt
+ | UnpTerminal s :: fmt when String.equal s (string_of_id ldots_var) -> List.rev hd, fmt
| u :: fmt ->
check_no_ldots_in_box u;
split_format_at_ldots (u::hd) fmt
@@ -559,7 +560,7 @@ let read_recursive_format sl fmt =
let sl = skip_var_in_recursive_format fmt in
try split_format_at_ldots [] sl with Exit -> error_format () in
let rec get_tail = function
- | a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt)
+ | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
| [], tail -> skip_var_in_recursive_format tail
| _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in
let slfmt, fmt = get_head fmt in
@@ -568,12 +569,12 @@ let read_recursive_format sl fmt =
let hunks_of_format (from,(vars,typs)) symfmt =
let rec aux = function
| symbs, (UnpTerminal s' as u) :: fmt
- when s' = String.make (String.length s') ' ' ->
+ when String.equal s' (String.make (String.length s') ' ') ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
| Terminal s :: symbs, (UnpTerminal s') :: fmt
- when s = String.drop_simple_quotes s' ->
+ when String.equal s (String.drop_simple_quotes s') ->
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
- | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
+ | NonTerminal s :: symbs, UnpTerminal s' :: fmt when id_eq s (id_of_string s') ->
let i = List.index s vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
@@ -589,7 +590,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let _,prec = precedence_of_entry_type from typ in
let slfmt,fmt = read_recursive_format sl fmt in
let sl, slfmt = aux (sl,slfmt) in
- if sl <> [] then error_format ();
+ if not (List.is_empty sl) then error_format ();
let symbs, l = aux (symbs,fmt) in
let hunk = match typ with
| ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
@@ -637,7 +638,7 @@ let distribute a ll = List.map (fun l -> a @ l) ll
(* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep)
as many times as expected in [n] argument *)
let rec expand_list_rule typ tkl x n i hds ll =
- if i = n then
+ if Int.equal i n then
let hds =
GramConstrListMark (n,true) :: hds
@ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
@@ -678,7 +679,7 @@ let make_production etyps symbols =
let rec find_symbols c_current c_next c_last = function
| [] -> []
| NonTerminal id :: sl ->
- let prec = if sl <> [] then c_current else c_last in
+ let prec = if not (List.is_empty sl) then c_current else c_last in
(id, prec) :: (find_symbols c_next c_next c_last sl)
| Terminal s :: sl -> find_symbols c_next c_next c_last sl
| Break n :: sl -> find_symbols c_current c_next c_last sl
@@ -700,10 +701,10 @@ let recompute_assoc typs =
(* Registration of syntax extensions (parsing/printing, no interpretation)*)
let pr_arg_level from = function
- | (n,L) when n=from -> str "at next level"
+ | (n,L) when Int.equal n from -> str "at next level"
| (n,E) -> str "at level " ++ int n
| (n,L) -> str "at level below " ++ int n
- | (n,Prec m) when m=n -> str "at level " ++ int n
+ | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
| (n,_) -> str "Unknown level"
let pr_level ntn (from,args) =
@@ -732,7 +733,7 @@ let cache_one_syntax_extension se =
let prec = se.synext_level in
try
let oldprec = Notation.level_of_notation ntn in
- if prec <> oldprec then error_incompatible_level ntn oldprec prec
+ if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
with Not_found ->
(* Reserve the notation level *)
Notation.declare_notation_level ntn prec;
@@ -789,22 +790,22 @@ let interp_modifiers modl =
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
| SetLevel n :: l ->
- if level <> None then error "A level is given more than once.";
+ if not (Option.is_empty level) then error "A level is given more than once.";
interp assoc (Some n) etyps format l
| SetAssoc a :: l ->
- if assoc <> None then error"An associativity is given more than once.";
+ if not (Option.is_empty assoc) then error"An associativity is given more than once.";
interp (Some a) level etyps format l
| SetOnlyParsing _ :: l ->
onlyparsing := true;
interp assoc level etyps format l
| SetFormat s :: l ->
- if format <> None then error "A format is given more than once.";
+ if not (Option.is_empty format) then error "A format is given more than once.";
interp assoc level etyps (Some s) l
in interp None None [] None modl
let check_infix_modifiers modifiers =
let (assoc,level,t,b,fmt) = interp_modifiers modifiers in
- if t <> [] then
+ if not (List.is_empty t) then
error "Explicit entry level or type unexpected in infix notation."
let no_syntax_modifiers = function
@@ -837,7 +838,7 @@ let join_auxiliary_recursive_types recvars etyps =
| None, None -> typs
| Some _, None -> typs
| None, Some ytyp -> (x,ytyp)::typs
- | Some xtyp, Some ytyp when xtyp = ytyp -> typs
+ | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
| Some xtyp, Some ytyp ->
errorlabstrm ""
(strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
@@ -867,8 +868,12 @@ let make_interpretation_type isrec = function
| NtnInternTypeBinder -> error "Type not allowed in recursive notation."
let make_interpretation_vars recvars allvars =
+ let eq_subscope (sc1, l1) (sc2, l2) =
+ Option.Misc.compare String.equal sc1 sc2 &&
+ List.equal String.equal l1 l2
+ in
List.iter (fun (x,y) ->
- if fst (List.assoc x allvars) <> fst (List.assoc y allvars) then
+ if not (eq_subscope (fst (List.assoc x allvars)) (fst (List.assoc y allvars))) then
error_not_same_scope x y) recvars;
let useless_recvars = List.map snd recvars in
let mainvars =
@@ -893,31 +898,32 @@ let find_precedence lev etyps symbols =
| ETConstr _ ->
error "The level of the leftmost non-terminal cannot be changed."
| ETName | ETBigint | ETReference ->
- if lev = None then
+ begin match lev with
+ | None ->
([msg_info,strbrk "Setting notation at level 0."],0)
- else
- if lev <> Some 0 then
+ | Some 0 ->
+ ([],0)
+ | _ ->
error "A notation starting with an atomic expression must be at level 0."
- else
- ([],0)
+ end
| ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
- if lev = None then
+ if Option.is_empty lev then
error "Need an explicit level."
else [],Option.get lev
| ETConstrList _ | ETBinderList _ ->
assert false (* internally used in grammar only *)
with Not_found ->
- if lev = None then
+ if Option.is_empty lev then
error "A left-recursive notation must have an explicit level."
else [],Option.get lev)
| Terminal _ ::l when
(match List.last symbols with Terminal _ -> true |_ -> false)
->
- if lev = None then
+ if Option.is_empty lev then
([msg_info,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| _ ->
- if lev = None then error "Cannot determine the level.";
+ if Option.is_empty lev then error "Cannot determine the level.";
[],Option.get lev
let check_curly_brackets_notation_exists () =
@@ -940,9 +946,9 @@ let remove_curly_brackets l =
let br',next' = skip_break [] l' in
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
- if l <> l0 or l' <> l1 then
+ if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
msg_warning (strbrk "Skipping spaces inside curly brackets");
- if deb & l'' = [] then [t1;x;t2] else begin
+ if deb && List.is_empty l'' then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
end
@@ -958,7 +964,7 @@ let compute_syntax_data df modifiers =
let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
- let need_squash = (symbols <> symbols') in
+ let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in
let ntn_for_grammar = make_notation_key symbols' in
check_rule_productivity symbols';
let msgs,n = find_precedence n etyps symbols' in
@@ -1050,11 +1056,11 @@ let with_syntax_protection f x =
(* Recovering existing syntax *)
let contract_notation ntn =
- if ntn = "{ _ }" then ntn else
+ if String.equal ntn "{ _ }" then ntn else
let rec aux ntn i =
if i <= String.length ntn - 5 then
let ntn' =
- if String.sub ntn i 5 = "{ _ }" then
+ if String.equal (String.sub ntn i 5) "{ _ }" then
String.sub ntn 0 i ^ "_" ^
String.sub ntn (i+5) (String.length ntn -i-5)
else ntn in
@@ -1084,7 +1090,7 @@ let recover_squash_syntax sy =
let recover_notation_syntax rawntn =
let ntn = contract_notation rawntn in
let sy = recover_syntax ntn in
- let need_squash = ntn <> rawntn in
+ let need_squash = not (String.equal ntn rawntn) in
let rules = if need_squash then recover_squash_syntax sy else [sy] in
sy.synext_intern, rules
@@ -1242,7 +1248,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with
| ScopeClasses cl ->
let cl' = List.map_filter (subst_scope_class subst) cl in
let cl' =
- if List.length cl = List.length cl' && List.for_all2 (==) cl cl' then cl
+ if Int.equal (List.length cl) (List.length cl') && List.for_all2 (==) cl cl' then cl
else cl' in
scope, ScopeClasses cl'
| _ -> x
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 9987de85a..8604b2ef2 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -49,7 +49,7 @@ open System
let coq_mlpath_copy = ref ["."]
let keep_copy_mlpath path =
let cpath = canonical_path_name path in
- let filter path' = (cpath <> canonical_path_name path') in
+ let filter path' = not (String.equal cpath (canonical_path_name path')) in
coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
(* If there is a toplevel under Coq *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 5210a3c9e..9b549084a 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -234,14 +234,14 @@ let eterm_obligations env name evm fs ?status t ty =
let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in
let status, chop = match status with
| Some (Evar_kinds.Define true as stat) ->
- if chop <> fs then Evar_kinds.Define false, None
+ if not (Int.equal chop fs) then Evar_kinds.Define false, None
else stat, Some chop
| Some s -> s, None
| None -> Evar_kinds.Define true, None
in
let tac = match evar_tactic.get ev.evar_extra with
| Some t ->
- if Dyn.tag t = "tactic" then
+ if String.equal (Dyn.tag t) "tactic" then
Some (Tacinterp.interp
(Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
else None
@@ -369,7 +369,7 @@ let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
let get_obligation_body expand obl =
let c = Option.get obl.obl_body in
- if expand && obl.obl_status = Evar_kinds.Expand then
+ if expand && obl.obl_status == Evar_kinds.Expand then
match kind_of_term c with
| Const c -> constant_value (Global.env ()) c
| _ -> c
@@ -471,7 +471,7 @@ let close sec =
errorlabstrm "Program"
(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
- (str (if List.length keys = 1 then " has " else "have ") ++
+ (str (if Int.equal (List.length keys) 1 then " has " else "have ") ++
str "unsolved obligations"))
let input : program_info ProgMap.t -> obj =
@@ -518,9 +518,10 @@ open Pp
let rec lam_index n t acc =
match kind_of_term t with
- | Lambda (na, _, b) ->
- if na = Name n then acc
- else lam_index n b (succ acc)
+ | Lambda (Name n', _, _) when id_eq n n' ->
+ acc
+ | Lambda (_, _, b) ->
+ lam_index n b (succ acc)
| _ -> raise Not_found
let compute_possible_guardness_evidences (n,_) fixbody fixtype =
@@ -553,7 +554,7 @@ let declare_mutual_definition l =
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
let (local,kind) = first.prg_kind in
let fixnames = first.prg_deps in
- let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
+ let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
| IsFixpoint wfl ->
@@ -568,7 +569,7 @@ let declare_mutual_definition l =
let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
- Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
first.prg_hook local gr;
@@ -600,7 +601,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
- assert(obls = [||]);
+ assert(Int.equal (Array.length obls) 0);
let n = Nameops.add_suffix n "_obligation" in
[| { obl_name = n; obl_body = None;
obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
@@ -682,7 +683,7 @@ let update_obls prg obls rem =
Defined (ConstRef kn)
else Dependent)
-let is_defined obls x = obls.(x).obl_body <> None
+let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
let deps_remaining obls deps =
Intset.fold
@@ -695,7 +696,7 @@ let dependencies obls n =
let res = ref Intset.empty in
Array.iteri
(fun i obl ->
- if i <> n && Intset.mem n obl.obl_deps then
+ if not (Int.equal i n) && Intset.mem n obl.obl_deps then
res := Intset.add i !res)
obls;
!res
@@ -740,7 +741,7 @@ let rec solve_obligation prg num tac =
let user_num = succ num in
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
- if obl.obl_body <> None then
+ if not (Option.is_empty obl.obl_body) then
pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
else
match deps_remaining obls obl.obl_deps with
@@ -773,7 +774,7 @@ let rec solve_obligation prg num tac =
match res with
| Remain n when n > 0 ->
let deps = dependencies obls num in
- if deps <> Intset.empty then
+ if not (Intset.is_empty deps) then
ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
| _ -> ());
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
@@ -801,7 +802,7 @@ and solve_obligation_by_tac prg obls i tac =
| Some _ -> false
| None ->
try
- if deps_remaining obls obl.obl_deps = [] then
+ if List.is_empty (deps_remaining obls obl.obl_deps) then
let obl = subst_deps_obl obls obl in
let tac =
match tac with
@@ -970,7 +971,7 @@ let next_obligation n tac =
| Some _ -> get_prog_err n
in
let obls, rem = prg.prg_obligations in
- let is_open _ x = x.obl_body = None && deps_remaining obls x.obl_deps = [] in
+ let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
let i = match Array.findi is_open obls with
| Some i -> i
| None -> anomaly "Could not find a solvable obligation."
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 85abcc01c..27f63d2f8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -56,10 +56,9 @@ let typecheck_params_and_fields id t ps nots fs =
let evars = ref Evd.empty in
let _ =
let error bk (loc, name) =
- match bk with
- | Default _ ->
- if name = Anonymous then
- user_err_loc (loc, "record", str "Record parameters must be named")
+ match bk, name with
+ | Default _, Anonymous ->
+ user_err_loc (loc, "record", str "Record parameters must be named")
| _ -> ()
in
List.iter
@@ -153,7 +152,7 @@ let subst_projection fid l c =
in
let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
let c'' = substrec 0 c' in
- if !bad_projs <> [] then
+ if not (List.is_empty !bad_projs) then
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
@@ -222,7 +221,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
- (nfi-1,(fi, optci=None)::kinds,sp_projs,subst))
+ (nfi-1,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
(List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
@@ -266,7 +265,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
let mie =
{ mind_entry_params = List.map degenerate_decl params;
mind_entry_record = true;
- mind_entry_finite = finite<>CoFinite;
+ mind_entry_finite = finite != CoFinite;
mind_entry_inds = [mie_ind] } in
let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
@@ -383,7 +382,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
| _ -> acc in
let allnames = idstruc::(List.fold_left extract_name [] fs) in
if not (List.distinct allnames) then error "Two objects have the same name";
- if not (kind = Class false) && List.exists ((<>) None) priorities then
+ let isnot_class = match kind with Class false -> false | _ -> true in
+ if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
error "Priorities only allowed for type class substructures";
(* Now, younger decl in params and fields is on top *)
let sc = interp_and_check_sort s in
@@ -402,6 +402,6 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
let implfs = List.map
(fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs
- fields is_coe (List.map (fun coe -> coe <> None) coers) sign in
+ fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
IndRef ind
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 23e4596b0..ab3b9b728 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -61,18 +61,24 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
| "VARIABLE" ->
(try
let (id,_,typ) = Global.lookup_named (basename sp) in
- if refopt = None
- || head_const typ = constr_of_global (Option.get refopt)
- then
+ begin match refopt with
+ | None ->
+ fn (VarRef id) env typ
+ | Some r when eq_constr (head_const typ) (constr_of_global r) ->
fn (VarRef id) env typ
+ | _ -> ()
+ end
with Not_found -> (* we are in a section *) ())
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
let typ = Typeops.type_of_constant env cst in
- if refopt = None
- || head_const typ = constr_of_global (Option.get refopt)
- then
- fn (ConstRef cst) env typ
+ begin match refopt with
+ | None ->
+ fn (ConstRef cst) env typ
+ | Some r when eq_constr (head_const typ) (constr_of_global r) ->
+ fn (ConstRef cst) env typ
+ | _ -> ()
+ end
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
@@ -242,7 +248,7 @@ let search_about_item (itemref,typ) = function
let raw_search_about filter_modules display_function l =
let filter ref' env typ =
filter_modules ref' env typ &&
- List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l &&
+ List.for_all (fun (b,i) -> (b : bool) == search_about_item (ref',typ) i) l &&
filter_blacklist ref' () ()
in
gen_filtered_search filter display_function
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 175a95165..479e14c8d 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -116,7 +116,7 @@ let blanch_utf8_string s bp ep =
fixed-size char and therefore contract all utf-8 code into one
space; in any case, preserve tabulation so
that its effective interpretation in terms of spacing is preserved *)
- if s.[i] = '\t' then s'.[!j] <- '\t';
+ if s.[i] == '\t' then s'.[!j] <- '\t';
if n < 0x80 || 0xC0 <= n then incr j
done;
String.sub s' 0 !j
@@ -152,11 +152,11 @@ let print_highlight_location ib loc =
let print_location_in_file s inlibrary fname loc =
let errstrm = str"Error while reading " ++ str s in
- if loc = Loc.ghost then
+ if Loc.is_ghost loc then
hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
else
let errstrm =
- if s = fname then mt() else errstrm ++ str":" ++ fnl() in
+ if String.equal s fname then mt() else errstrm ++ str":" ++ fnl() in
if inlibrary then
hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
@@ -183,15 +183,15 @@ let print_location_in_file s inlibrary fname loc =
hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
let valid_loc dloc loc =
- loc <> Loc.ghost
- & match dloc with
+ not (Loc.is_ghost loc)
+ && match dloc with
| Some dloc ->
- let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b & e<=ed
+ let (bd,ed) = Loc.unloc dloc in let (b,e) = Loc.unloc loc in bd<=b && e<=ed
| _ -> true
let valid_buffer_loc ib dloc loc =
valid_loc dloc loc &
- let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e
+ let (b,e) = Loc.unloc loc in b-ib.start >= 0 & e-ib.start < ib.len && b<=e
(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
otherwise. We trap all exceptions to prevent the error message printing
@@ -228,7 +228,7 @@ let make_emacs_prompt() =
let pending = Pfedit.get_all_proof_names() in
let pendingprompt =
List.fold_left
- (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
+ (fun acc x -> acc ^ (if String.equal acc "" then "" else "|") ^ Names.string_of_id x)
"" pending in
let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
@@ -274,7 +274,7 @@ let print_toplevel_error exc =
let (dloc,exc) =
match exc with
| DuringCommandInterp (loc,ie) ->
- if loc = Loc.ghost then (None,ie) else (Some loc, ie)
+ if Loc.is_ghost loc then (None,ie) else (Some loc, ie)
| _ -> (None, exc)
in
let (locstrm,exc) =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 42b9411f8..34aa23585 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -104,9 +104,9 @@ let raise_with_file file exc =
in
let (inner,inex) =
match re with
- | Error_in_file (_, (b,f,loc), e) when loc <> Loc.ghost ->
+ | Error_in_file (_, (b,f,loc), e) when not (Loc.is_ghost loc) ->
((b, f, loc), e)
- | Loc.Exc_located (loc, e) when loc <> Loc.ghost ->
+ | Loc.Exc_located (loc, e) when not (Loc.is_ghost loc) ->
((false,file, loc), e)
| Loc.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
in
@@ -430,7 +430,8 @@ let compile verbosely f =
Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
if !Flags.xml_export then !xml_start_library ();
let _ = load_vernac verbosely long_f_dot_v in
- if Pfedit.get_all_proof_names () <> [] then
+ let pfs = Pfedit.get_all_proof_names () in
+ if not (List.is_empty pfs) then
(pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
if !Flags.xml_export then !xml_end_library ();
Dumpglob.end_dump_glob ();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 44120dcb3..71ae8a1ec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -77,7 +77,7 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
else if ng < ngprev then
(* A subgoal have been solved. Let's compute the new current level
by discarding all levels with 0 remaining goals. *)
- let _ = assert (ng = ngprev - 1) in
+ let _ = assert (Int.equal ng (ngprev - 1)) in
let rec loop = function
| (0, ng2::ngl2) -> loop (ng2,ngl2)
| p -> p
@@ -306,7 +306,9 @@ let print_namespace ns =
in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
in
- let matches mp = match_modulepath ns mp = Some [] in
+ let matches mp = match match_modulepath ns mp with
+ | Some [] -> true
+ | _ -> false in
let constants = (Environ.pre_env (Global.env ())).Pre_env.env_globals.Pre_env.env_constants in
let constants_in_namespace =
Cmap_env.fold (fun c (body,_) acc ->
@@ -398,7 +400,7 @@ let print_located_module r =
let dir = Nametab.full_name_module qid in
msg_notice (str "Module " ++ pr_dirpath dir)
with Not_found ->
- if fst (repr_qualid qid) = empty_dirpath then
+ if dir_path_eq (fst (repr_qualid qid)) empty_dirpath then
msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid)
else
msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid)
@@ -448,7 +450,7 @@ let start_proof_and_print k l hook =
print_subgoals ()
let vernac_definition (local,k) (loc,id as lid) def hook =
- if local = Local then Dumpglob.dump_definition lid true "var"
+ if local == Local then Dumpglob.dump_definition lid true "var"
else Dumpglob.dump_definition lid false "def";
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
@@ -504,7 +506,7 @@ let vernac_exact_proof c =
Backtrack.mark_unreachable [prf]
let vernac_assumption kind l nl=
- let global = fst kind = Global in
+ let global = (fst kind) == Global in
let status =
List.fold_left (fun status (is_coe,(idl,c)) ->
if Dumpglob.dump () then
@@ -560,7 +562,7 @@ let vernac_inductive finite infer indl =
| _ -> Errors.error "Cannot handle mutually (co)inductive records."
in
let indl = List.map unpack indl in
- do_mutual_inductive indl (finite<>CoFinite)
+ do_mutual_inductive indl (finite != CoFinite)
let vernac_fixpoint l =
if Dumpglob.dump () then
@@ -605,7 +607,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
error "Modules and Module Types are not allowed inside sections.";
let binders_ast = List.map
(fun (export,idl,ty) ->
- if export <> None then
+ if not (Option.is_empty export) then
error ("Arguments of a functor declaration cannot be exported. " ^
"Remove the \"Export\" and \"Import\" keywords from every functor " ^
"argument.")
@@ -646,7 +648,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
| _::_ ->
let binders_ast = List.map
(fun (export,idl,ty) ->
- if export <> None then
+ if not (Option.is_empty export) then
error ("Arguments of a functor definition can be imported only if" ^
" the definition is interactive. Remove the \"Export\" and " ^
"\"Import\" keywords from every functor argument.")
@@ -695,7 +697,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
| _ :: _ ->
let binders_ast = List.map
(fun (export,idl,ty) ->
- if export <> None then
+ if not (Option.is_empty export) then
error ("Arguments of a functor definition can be imported only if" ^
" the definition is interactive. Remove the \"Export\" " ^
"and \"Import\" keywords from every functor argument.")
@@ -812,7 +814,9 @@ let vernac_solve_existential = instantiate_nth_evar_com
let vernac_set_end_tac tac =
if not (refining ()) then
error "Unknown command of the non proof-editing mode.";
- if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
+ match tac with
+ | Tacexpr.TacId [] -> ()
+ | _ -> set_end_tac (Tacinterp.interp tac)
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
let vernac_set_used_variables l =
@@ -820,7 +824,7 @@ let vernac_set_used_variables l =
if not (List.distinct l) then error "Used variables list contains duplicates";
let vars = Environ.named_context (Global.env ()) in
List.iter (fun id ->
- if not (List.exists (fun (id',_,_) -> id = id') vars) then
+ if not (List.exists (fun (id',_,_) -> id_eq id id') vars) then
error ("Unknown variable: " ^ string_of_id id))
l;
set_used_variables l
@@ -903,9 +907,9 @@ let vernac_declare_arguments local r l nargs flags =
let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
let names, rest = List.hd names, List.tl names in
let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
- if List.exists ((<>) names) rest then
+ if List.exists (fun na -> not (List.equal name_eq na names)) rest then
error "All arguments lists must declare the same names.";
- if not (Util.List.distinct (List.filter ((<>) Anonymous) names)) then
+ if not (List.distinct (List.filter ((!=) Anonymous) names)) then
error "Arguments names must be distinct.";
let sr = smart_global r in
let inf_names =
@@ -921,39 +925,48 @@ let vernac_declare_arguments local r l nargs flags =
(String.concat ", " (List.map string_of_name l)) ^ ".")
| _::li, _::ld, _::ls -> check li ld ls
| _ -> assert false in
- if l <> [[]] then
- List.iter2 (fun l -> check inf_names l) (names :: rest) scopes;
+ let () = match l with
+ | [[]] -> ()
+ | _ ->
+ List.iter2 (fun l -> check inf_names l) (names :: rest) scopes
+ in
(* we take extra scopes apart, and we check they are consistent *)
let l, scopes =
let scopes, rest = List.hd scopes, List.tl scopes in
- if List.exists (List.exists ((<>) None)) rest then
+ if List.exists (List.exists ((!=) None)) rest then
error "Notation scopes can be given only once";
if not extra_scope_flag then l, scopes else
let l, _ = List.split (List.map (List.chop (List.length inf_names)) l) in
l, scopes in
(* we interpret _ as the inferred names *)
- let l = if l = [[]] then l else
+ let l = match l with
+ | [[]] -> l
+ | _ ->
let name_anons = function
| (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d
| x, _ -> x in
List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in
let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
let some_renaming_specified =
- try Arguments_renaming.arguments_names sr <> names_decl
+ try
+ let names = Arguments_renaming.arguments_names sr in
+ not (List.equal (List.equal name_eq) names names_decl)
with Not_found -> false in
let some_renaming_specified, implicits =
- if l = [[]] then false, [[]] else
- Util.List.fold_map (fun sr il ->
- let sr', impl = Util.List.fold_map (fun b -> function
+ match l with
+ | [[]] -> false, [[]]
+ | _ ->
+ List.fold_map (fun sr il ->
+ let sr', impl = List.fold_map (fun b -> function
| (Anonymous, _,_, true, max), Name id -> assert false
| (Name x, _,_, true, _), Anonymous ->
error ("Argument "^string_of_id x^" cannot be declared implicit.")
| (Name iid, _,_, true, max), Name id ->
- b || iid <> id, Some (ExplByName id, max, false)
- | (Name iid, _,_, _, _), Name id -> b || iid <> id, None
+ b || not (id_eq iid id), Some (ExplByName id, max, false)
+ | (Name iid, _,_, _, _), Name id -> b || not (id_eq iid id), None
| _ -> b, None)
sr (List.combine il inf_names) in
- sr || sr', Util.List.map_filter (fun x -> x) impl)
+ sr || sr', List.map_filter (fun x -> x) impl)
some_renaming_specified l in
if some_renaming_specified then
if not (List.mem `Rename flags) then
@@ -961,13 +974,14 @@ let vernac_declare_arguments local r l nargs flags =
else Arguments_renaming.rename_arguments local sr names_decl;
(* All other infos are in the first item of l *)
let l = List.hd l in
- let some_implicits_specified = implicits <> [[]] in
+ let some_implicits_specified = match implicits with
+ | [[]] -> false | _ -> true in
let scopes = List.map (function
| None -> None
| Some (o, k) ->
try Some(ignore(Notation.find_scope k); k)
with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
- let some_scopes_specified = List.exists ((<>) None) scopes in
+ let some_scopes_specified = List.exists ((!=) None) scopes in
let rargs =
Util.List.map_filter (function (n, true) -> Some n | _ -> None)
(Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
@@ -983,7 +997,7 @@ let vernac_declare_arguments local r l nargs flags =
| #Tacred.simpl_flag as x :: tl -> x :: narrow tl
| [] -> [] | _ :: tl -> narrow tl in
let flags = narrow flags in
- if rargs <> [] || nargs >= 0 || flags <> [] then
+ if not (List.is_empty rargs) || nargs >= 0 || not (List.is_empty flags) then
match sr with
| ConstRef _ as c ->
Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
@@ -1238,7 +1252,7 @@ let _ =
optdepr = false;
optname = "Ltac debug";
optkey = ["Ltac";"Debug"];
- optread = (fun () -> get_debug () <> Tactic_debug.DebugOff);
+ optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
let _ =
@@ -1451,7 +1465,7 @@ let vernac_locate = function
let vernac_backto lbl =
try
let lbl' = Backtrack.backto lbl in
- if lbl <> lbl' then
+ if not (Int.equal lbl lbl') then
Pp.msg_warning
(str "Actually back to state "++ Pp.int lbl' ++ str ".");
try_print_subgoals ()
@@ -1460,7 +1474,7 @@ let vernac_backto lbl =
let vernac_back n =
try
let extra = Backtrack.back n in
- if extra <> 0 then
+ if not (Int.equal extra 0) then
Pp.msg_warning
(str "Actually back by " ++ Pp.int (extra+n) ++ str " steps.");
try_print_subgoals ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 23:34:11 +0000