aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorppedrot2012-11-25 17:39:18 +0000
committerppedrot2012-11-25 17:39:18 +0000
commit31dbba5f5c16f81c6dac2adaba46087da787ac12 (patch)
treea3402adb697f4272a859028590ec0a905709327e
parentde5bd6a09e2323faf4ac4b7576d55c3d2cb94ba7 (diff)
Monomorphization (tactics)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16003 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--tactics/auto.ml68
-rw-r--r--tactics/autorewrite.ml10
-rw-r--r--tactics/btermdn.ml1
-rw-r--r--tactics/class_tactics.ml422
-rw-r--r--tactics/dn.ml3
-rw-r--r--tactics/eauto.ml418
-rw-r--r--tactics/eqschemes.ml22
-rw-r--r--tactics/equality.ml43
-rw-r--r--tactics/evar_tactics.ml1
-rw-r--r--tactics/extratactics.ml410
-rw-r--r--tactics/hipattern.ml467
-rw-r--r--tactics/inv.ml31
-rw-r--r--tactics/refine.ml6
-rw-r--r--tactics/rewrite.ml436
-rw-r--r--tactics/tacintern.ml14
-rw-r--r--tactics/tacinterp.ml65
-rw-r--r--tactics/tacsubst.ml2
-rw-r--r--tactics/tacticals.ml10
-rw-r--r--tactics/tactics.ml160
-rw-r--r--tactics/tauto.ml42
20 files changed, 326 insertions, 265 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8daf11c705..b626e662d2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,7 +117,7 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t
let empty_se = ([],[],Bounded_net.create ())
let eq_pri_auto_tactic (_, x) (_, y) =
- if x.pri = y.pri && x.pat = y.pat then
+ if Int.equal x.pri y.pri && Option.Misc.compare constr_pattern_eq x.pat y.pat then
match x.code,y.code with
| Res_pf(cstr,_),Res_pf(cstr1,_) ->
eq_constr cstr cstr1
@@ -173,13 +173,29 @@ let translate_hint (go,p) =
in
(go,{ p with code = code })
+let hints_path_atom_eq h1 h2 = match h1, h2 with
+| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
+| PathAny, PathAny -> true
+| _ -> false
+
+let rec hints_path_eq h1 h2 = match h1, h2 with
+| PathAtom h1, PathAtom h2 -> hints_path_atom_eq h1 h2
+| PathStar h1, PathStar h2 -> hints_path_eq h1 h2
+| PathSeq (l1, r1), PathSeq (l2, r2) ->
+ hints_path_eq l1 l2 && hints_path_eq r1 r2
+| PathOr (l1, r1), PathOr (l2, r2) ->
+ hints_path_eq l1 l2 && hints_path_eq r1 r2
+| PathEmpty, PathEmpty -> true
+| PathEpsilon, PathEpsilon -> true
+| _ -> false
+
let path_matches hp hints =
let rec aux hp hints k =
match hp, hints with
| PathAtom _, [] -> false
| PathAtom PathAny, (_ :: hints') -> k hints'
| PathAtom p, (h :: hints') ->
- if p = h then k hints' else false
+ if hints_path_atom_eq p h then k hints' else false
| PathStar hp', hints ->
k hints || aux hp' hints (fun hints' -> aux hp hints' k)
| PathSeq (hp, hp'), hints ->
@@ -209,7 +225,7 @@ let rec is_empty = function
let rec path_derivate hp hint =
let rec derivate_atoms hints hints' =
match hints, hints' with
- | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs'
+ | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs'
| [], [] -> PathEpsilon
| [], hints -> PathEmpty
| grs, [] -> PathAtom (PathHints grs)
@@ -242,11 +258,11 @@ let rec normalize_path h =
| PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
| PathOr (p, q) ->
let p', q' = normalize_path p, normalize_path q in
- if p = p' && q = q' then h
+ if hints_path_eq p p' && hints_path_eq q q' then h
else normalize_path (PathOr (p', q'))
| PathSeq (p, q) ->
let p', q' = normalize_path p, normalize_path q in
- if p = p' && q = q' then h
+ if hints_path_eq p p' && hints_path_eq q q' then h
else normalize_path (PathSeq (p', q'))
| _ -> h
@@ -347,7 +363,7 @@ module Hint_db = struct
let pat = if not db.use_dn && is_exact v.code then None else v.pat in
match k with
| None ->
- if not (List.exists (fun (_, (_, v')) -> v = v') db.hintdb_nopat) then
+ if not (List.exists (fun (_, (_, v')) -> Pervasives.(=) v v') db.hintdb_nopat) then (** FIXME *)
{ db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
else db
| Some gr ->
@@ -496,7 +512,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty)
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
let nmiss = List.length (clenv_missing ce) in
- if nmiss = 0 then
+ if Int.equal nmiss 0 then
(Some hd,
{ pri = (match pri with None -> nb_hyp cty | Some p -> p);
pat = Some pat;
@@ -526,7 +542,7 @@ let make_resolves env sigma flags pri ?name c =
let ents = List.map_filter try_apply
[make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
in
- if ents = [] then
+ if List.is_empty ents then
errorlabstrm "Hint"
(pr_lconstr c ++ spc() ++
(if pi1 flags then str"cannot be used as a hint."
@@ -689,7 +705,9 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
if path' == path then obj else (local, name, AddCut path')
let classify_autohint ((local,name,hintlist) as obj) =
- if local or hintlist = (AddHints []) then Dispose else Substitute obj
+ match hintlist with
+ | AddHints [] -> Dispose
+ | _ -> if local then Dispose else Substitute obj
let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
@@ -702,7 +720,7 @@ let create_hint_db l n st b =
Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
let remove_hints local dbnames grs =
- let dbnames = if dbnames = [] then ["core"] else dbnames in
+ let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
List.iter
(fun dbname ->
Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
@@ -799,7 +817,7 @@ let prepare_hint env (sigma,c) =
(* We skip the test whether args is the identity or not *)
let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
- if free_rels t <> Intset.empty then
+ if not (Intset.is_empty (free_rels t)) then
error "Hints with holes dependent on a bound variable not supported.";
if occur_existential t then
(* Not clever enough to construct dependency graph of evars *)
@@ -870,7 +888,7 @@ let interp_hints =
let add_hints local dbnames0 h =
if List.mem "nocore" dbnames0 then
error "The hint database \"nocore\" is meant to stay empty.";
- let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
+ let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
let env = Global.env() and sigma = Evd.empty in
match h with
| HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
@@ -905,7 +923,7 @@ let pr_hint_list hintlist =
let pr_hints_db (name,db,hintlist) =
(str "In the database " ++ str name ++ str ":" ++
- if hintlist = [] then (str " nothing" ++ fnl ())
+ if List.is_empty hintlist then (str " nothing" ++ fnl ())
else (fnl () ++ pr_hint_list hintlist))
(* Print all hints associated to head c in any database *)
@@ -916,7 +934,7 @@ let pr_hint_list_for_head c =
(name, db, hints)
in
let valid_dbs = List.map validate dbs in
- if valid_dbs = [] then
+ if List.is_empty valid_dbs then
(str "No hint declared for :" ++ pr_global c)
else
hov 0
@@ -942,7 +960,7 @@ let pr_hint_term cl =
let fn db = List.map (fun x -> 0, x) (fn db) in
List.map (fun (name, db) -> (name, db, fn db)) dbs
in
- if valid_dbs = [] then
+ if List.is_empty valid_dbs then
(str "No hint applicable for current goal")
else
(str "Applicable Hints :" ++ fnl () ++
@@ -1007,7 +1025,7 @@ let pr_searchtable () =
(* tactics with a trace mechanism for automatic search *)
(**************************************************************************)
-let priority l = List.filter (fun (_, hint) -> hint.pri = 0) l
+let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
(* tell auto not to reuse already instantiated metas in unification (for
compatibility, since otherwise, apply succeeds oftener) *)
@@ -1134,8 +1152,8 @@ let no_dbg () = (Off,0,ref [])
let mk_trivial_dbg debug =
let d =
- if debug = Debug || !global_debug_trivial then Debug
- else if debug = Info || !global_info_trivial then Info
+ if debug == Debug || !global_debug_trivial then Debug
+ else if debug == Info || !global_info_trivial then Info
else Off
in (d,0,ref [])
@@ -1144,8 +1162,8 @@ let mk_trivial_dbg debug =
let mk_auto_dbg debug =
let d =
- if debug = Debug || !global_debug_auto then Debug
- else if debug = Info || !global_info_auto then Info
+ if debug == Debug || !global_debug_auto then Debug
+ else if debug == Info || !global_info_auto then Info
else Off
in (d,1,ref [])
@@ -1194,7 +1212,7 @@ let rec cleanup_info_trace depth acc = function
and erase_subtree depth = function
| [] -> []
- | (d,_) :: l -> if d = depth then l else erase_subtree depth l
+ | (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
let pr_info_atom (d,pp) =
str (String.make d ' ') ++ pp () ++ str "."
@@ -1220,10 +1238,10 @@ let tclTRY_dbg d tac =
tclORELSE0
(fun gl ->
let out = tac gl in
- if level <> Off then msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d);
+ if level != Off then msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d);
out)
(fun gl ->
- if level = Info then msg_debug (pr_info_nop d);
+ if level == Info then msg_debug (pr_info_nop d);
tclIDTAC gl)
(**************************************************************************)
@@ -1314,7 +1332,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
(unify_resolve_gen flags (c,cl))
(* With "(debug) trivial", we shouldn't end here, and
with "debug auto" we don't display the details of inner trivial *)
- (trivial_fail_db (no_dbg ()) (flags <> None) db_list local_db)
+ (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
(fun gl ->
if exists_evaluable_reference (pf_env gl) c then
@@ -1401,7 +1419,7 @@ let intro_register dbg kont db =
let search d n mod_delta db_list local_db =
let rec search d n local_db =
- if n=0 then (fun gl -> error "BOUND 2") else
+ if Int.equal n 0 then (fun gl -> error "BOUND 2") else
tclORELSE0 (dbg_assumption d)
(tclORELSE0 (intro_register d (search d n) local_db)
(fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e1a4d4f36e..bad5a6aa02 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -137,7 +137,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
g::_ ->
(match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
(lastid,_,_)::_ ->
- if last_hyp_id <> lastid then
+ if not (id_eq last_hyp_id lastid) then
begin
let gl'' =
if !to_be_cleared then
@@ -167,8 +167,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
let try_do_hyps treat_id l =
autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
in
- if cl.concl_occs <> AllOccurrences &
- cl.concl_occs <> NoOccurrences
+ if cl.concl_occs != AllOccurrences &&
+ cl.concl_occs != NoOccurrences
then
error "The \"at\" syntax isn't available yet for the autorewrite tactic."
else
@@ -178,7 +178,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
| _ -> tclTHENFIRST t1 t2
in
compose_tac
- (if cl.concl_occs <> NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC)
+ (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC)
(match cl.onhyps with
| Some l -> try_do_hyps (fun ((_,id),_) -> id) l
| None ->
@@ -191,7 +191,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC
let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
- let onconcl = cl.Locus.concl_occs <> NoOccurrences in
+ let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in
match onconcl,cl.Locus.onhyps with
| false,Some [_] | true,Some [] | false,Some [] ->
(* autorewrite with .... in clause using tac n'est sur que
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 819c76807a..875370501d 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Term
open Names
open Pattern
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f2f5417ef5..bc2e8ac2b5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -50,7 +50,7 @@ let evars_to_goals p evm =
(gls', Evd.add evm' ev evi'))
evm ([], Evd.defined_evars evm)
in
- if goals = [] then None else Some (List.rev goals, evm')
+ if List.is_empty goals then None else Some (List.rev goals, evm')
(** Typeclasses instance search tactic / eauto *)
@@ -80,7 +80,7 @@ let auto_unif_flags = {
let rec eq_constr_mod_evars x y =
match kind_of_term x, kind_of_term y with
- | Evar (e1, l1), Evar (e2, l2) when e1 <> e2 -> true
+ | Evar (e1, l1), Evar (e2, l2) when not (Int.equal e1 e2) -> true
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t gl =
@@ -107,7 +107,7 @@ let unify_resolve flags (c,clenv) gls =
Clenvtac.clenv_refine false ~with_classes:false clenv' gls
let clenv_of_prods nprods (c, clenv) gls =
- if nprods = 0 then Some clenv
+ if Int.equal nprods 0 then Some clenv
else
let ty = pf_type_of gls c in
let diff = nb_prod ty - nprods in
@@ -328,7 +328,7 @@ let compare (pri, _, _, res) (pri', _, _, res') =
List.length (sig_it s) + nb_empty_evars (sig_sig s)
in
let pri = pri - pri' in
- if pri <> 0 then pri
+ if not (Int.equal pri 0) then pri
else nbgoals res - nbgoals res'
let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
@@ -397,10 +397,12 @@ let hints_tac hints =
let isProp env sigma concl =
let ty = Retyping.get_type_of env sigma concl in
- kind_of_term ty = Sort (Prop Null)
+ match kind_of_term ty with
+ | Sort (Prop Null) -> true
+ | _ -> false
let needs_backtrack only_classes env evd oev concl =
- if oev = None || isProp env evd concl then
+ if Option.is_empty oev || isProp env evd concl then
not (Intset.is_empty (Evarutil.evars_of_term concl))
else true
@@ -413,7 +415,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
second.skft
(fun {it=gls';sigma=s'} fk' ->
let needs_backtrack =
- if gls' = [] then
+ if List.is_empty gls' then
needs_backtrack info.only_classes
(Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
else true
@@ -456,7 +458,7 @@ let rec fix (t : 'a tac) : 'a tac =
then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
let rec fix_limit limit (t : 'a tac) : 'a tac =
- if limit = 0 then fail_tac
+ if Int.equal limit 0 then fail_tac
else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
@@ -603,7 +605,7 @@ let error_unresolvable env comp do_split evd =
let _, ev = Evd.fold_undefined
(fun ev evi (b,acc) ->
(* focus on one instance if only one was searched for *)
- if class_of_constr evi.evar_concl <> None then
+ if not (Option.is_empty (class_of_constr evi.evar_concl)) then
if not b (* || do_split *) then
true, Some ev
else b, None
@@ -619,7 +621,7 @@ let error_unresolvable env comp do_split evd =
and return undefined evar_info *)
let select_and_update_evars p oevd in_comp evd ev evi =
- assert (evi.evar_body = Evar_empty);
+ assert (evi.evar_body == Evar_empty);
try
let oevi = Evd.find_undefined oevd ev in
if Typeclasses.is_resolvable oevi then
diff --git a/tactics/dn.ml b/tactics/dn.ml
index ea19ecc414..768cdf94e2 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -1,5 +1,4 @@
-
-
+open Util
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2bbb3ac5ac..4d037843e7 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -90,7 +90,7 @@ open Unification
(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
(***************************************************************************)
-let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
+let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
@@ -177,7 +177,7 @@ module SearchProblem = struct
type state = search_state
- let success s = (sig_it s.tacres) = []
+ let success s = List.is_empty (sig_it s.tacres)
let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
@@ -205,13 +205,13 @@ module SearchProblem = struct
let compare s s' =
let d = s'.depth - s.depth in
let nbgoals s = List.length (sig_it s.tacres) in
- if d <> 0 then d else nbgoals s - nbgoals s'
+ if not (Int.equal d 0) then d else nbgoals s - nbgoals s'
let branching s =
- if s.depth = 0 then
+ if Int.equal s.depth 0 then
[]
else
- let ps = if s.prev = Unknown then Unknown else State s in
+ let ps = if s.prev == Unknown then Unknown else State s in
let lg = s.tacres in
let nbgl = List.length (sig_it lg) in
assert (nbgl > 0);
@@ -292,8 +292,8 @@ let _ =
Goptions.optwrite = (:=) global_info_eauto }
let mk_eauto_dbg d =
- if d = Debug || !global_debug_eauto then Debug
- else if d = Info || !global_info_eauto then Info
+ if d == Debug || !global_debug_eauto then Debug
+ else if d == Info || !global_info_eauto then Info
else Off
let pr_info_nop = function
@@ -306,7 +306,7 @@ let pr_dbg_header = function
| Info -> msg_debug (str "(* info eauto : *)")
let pr_info dbg s =
- if dbg <> Info then ()
+ if dbg != Info then ()
else
let rec loop s =
match s.prev with
@@ -327,7 +327,7 @@ let make_initial_state dbg n gl dblist localdb =
last_tactic = lazy (mt());
dblist = dblist;
localdb = [localdb];
- prev = if dbg=Info then Init else Unknown;
+ prev = if dbg == Info then Init else Unknown;
}
let e_search_auto debug (in_depth,p) lems db_list gl =
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 33eb7c6185..5f6c776bab 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -94,14 +94,15 @@ let get_coq_eq () =
let get_sym_eq_data env ind =
let (mib,mip as specif) = lookup_mind_specif env ind in
- if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) ||
+ not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
- if List.exists (fun (_,b,_) -> b <> None) realsign then
+ if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported.";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+ if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
error "Constructor must have no arguments"; (* This can be relaxed... *)
let params,constrargs = List.chop mib.mind_nparams constrargs in
if mip.mind_nrealargs > mib.mind_nparams then
@@ -126,14 +127,15 @@ let get_sym_eq_data env ind =
let get_non_sym_eq_data env ind =
let (mib,mip as specif) = lookup_mind_specif env ind in
- if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) ||
+ not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
- if List.exists (fun (_,b,_) -> b <> None) realsign then
+ if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported";
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+ if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
error "Constructor must have no arguments";
let _,constrargs = List.chop mib.mind_nparams constrargs in
(specif,constrargs,realsign,mip.mind_nrealargs)
@@ -674,19 +676,19 @@ let rew_r2l_scheme_kind =
let build_congr env (eq,refl) ind =
let (mib,mip) = lookup_mind_specif env ind in
- if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+ if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
error "Not an inductive type with a single constructor.";
- if mip.mind_nrealargs <> 1 then
+ if not (Int.equal mip.mind_nrealargs 1) then
error "Expect an inductive type with one predicate parameter.";
let i = 1 in
let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
- if List.exists (fun (_,b,_) -> b <> None) realsign then
+ if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
error "Inductive equalities with local definitions in arity not supported.";
let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
let _,constrargs = decompose_app ccl in
- if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+ if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
error "Constructor must have no arguments";
let b = List.nth constrargs (i + mib.mind_nparams - 1) in
let varB = fresh env (id_of_string "B") in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 63cdbfa92c..ca54436a0f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -235,7 +235,7 @@ let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
eliminate lbeq on sort_of_gl. *)
let find_elim hdcncl lft2rgt dep cls args gl =
- let inccl = (cls = None) in
+ let inccl = Option.is_empty cls in
if (eq_constr hdcncl (constr_of_reference (Coqlib.glob_eq)) ||
eq_constr hdcncl (constr_of_reference (Coqlib.glob_jmeq)) &&
pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
@@ -245,9 +245,10 @@ let find_elim hdcncl lft2rgt dep cls args gl =
| Ind ind_sp ->
let pr1 =
lookup_eliminator ind_sp (elimination_sort_of_clause cls gl)
- in
- if lft2rgt = Some (cls=None)
- then
+ in
+ begin match lft2rgt, cls with
+ | Some true, None
+ | Some false, Some _ ->
let c1 = destConst pr1 in
let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in
let l' = label_of_id (add_suffix (id_of_label l) "_r") in
@@ -260,7 +261,8 @@ let find_elim hdcncl lft2rgt dep cls args gl =
let rwr_thm = string_of_label l' in
error ("Cannot find rewrite principle "^rwr_thm^".")
end
- else pr1
+ | _ -> pr1
+ end
| _ ->
(* cannot occur since we checked that we are in presence of
Logic.eq or Jmeq just before *)
@@ -313,7 +315,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
((c,l) : constr with_bindings) with_evars gl =
- if occs <> AllOccurrences then (
+ if occs != AllOccurrences then (
rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
else
let env = pf_env gl in
@@ -379,7 +381,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
(general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
(do_hyps l)
in
- if cl.concl_occs = NoOccurrences then do_hyps l else
+ if cl.concl_occs == NoOccurrences then do_hyps l else
tclTHENFIRST
(general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
(do_hyps l)
@@ -400,7 +402,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
Idset.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
in do_hyps_atleastonce ids gl
in
- if cl.concl_occs = NoOccurrences then do_hyps else
+ if cl.concl_occs == NoOccurrences then do_hyps else
tclIFTHENTRYELSEMUST
(general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
do_hyps
@@ -530,7 +532,7 @@ let find_positions env sigma t1 t2 =
match (kind_of_term hd1, kind_of_term hd2) with
| Construct sp1, Construct sp2
- when List.length args1 = mis_constructor_nargs_env env sp1
+ when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1)
->
let sorts = List.intersect sorts (allowed_sorts env (fst sp1)) in
(* both sides are fully applied constructors, so either we descend,
@@ -652,7 +654,7 @@ let descend_then sigma env head dirn =
let p =
it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
let build_branch i =
- let result = if i = dirn then dirnval else dfltval in
+ let result = if Int.equal i dirn then dirnval else dfltval in
it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
let brl =
List.map build_branch
@@ -696,7 +698,7 @@ let construct_discriminator sigma env dirn c sort =
let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
let cstrs = get_constructors env indf in
let build_branch i =
- let endpt = if i = dirn then true_0 else false_0 in
+ let endpt = if Int.equal i dirn then true_0 else false_0 in
it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
let brl =
List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
@@ -742,7 +744,7 @@ let ind_scheme_of_eq lbeq =
let kind = inductive_sort_family mip in
(* use ind rather than case by compatibility *)
let kind =
- if kind = InProp then Elimschemes.ind_scheme_kind_from_prop
+ if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
else Elimschemes.ind_scheme_kind_from_type in
mkConst (find_scheme kind (destInd lbeq.eq))
@@ -1088,7 +1090,7 @@ let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
with Failure _ -> None
in
let injectors = List.map_filter filter posns in
- if injectors = [] then
+ if List.is_empty injectors then
errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
tclTHEN
(tclMAP
@@ -1132,9 +1134,9 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
(* if yes, check if the user has declared the dec principle *)
(* and compare the fst arguments of the dep pair *)
let new_eq_args = [|type_of env sigma (ar1.(3));ar1.(3);ar2.(3)|] in
- if ( (eqTypeDest = sigTconstr()) &&
- (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind=true) &&
- (is_conv env sigma (ar1.(2)) (ar2.(2)) = true))
+ if ( (eq_constr eqTypeDest (sigTconstr())) &&
+ (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind) &&
+ (is_conv env sigma (ar1.(2)) (ar2.(2))))
then (
(* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
let qidl = qualid_of_reference
@@ -1388,7 +1390,8 @@ let unfold_body x gl =
let restrict_to_eq_and_identity eq = (* compatibility *)
- if eq <> constr_of_global glob_eq && eq <> constr_of_global glob_identity then
+ if not (eq_constr eq (constr_of_global glob_eq)) &&
+ not (eq_constr eq (constr_of_global glob_identity)) then
raise PatternMatchingFailure
exception FoundHyp of (identifier * constr * bool)
@@ -1409,7 +1412,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
(* The set of hypotheses using x *)
let depdecls =
let test (id,_,c as dcl) =
- if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then Some dcl
+ if not (id_eq id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl
else None in
List.rev (List.map_filter test (pf_hyps gl)) in
let dephyps = List.map (fun (id,_,_) -> id) depdecls in
@@ -1429,7 +1432,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
(replace_term (mkVar x) rhs hval)
(Some (replace_term (mkVar x) rhs htyp)) nowhere
in
- let need_rewrite = dephyps <> [] || depconcl in
+ let need_rewrite = not (List.is_empty dephyps) || depconcl in
tclTHENLIST
((if need_rewrite then
[generalize abshyps;
@@ -1447,7 +1450,7 @@ let subst_one_var dep_proof_ok x gl =
let hyps = pf_hyps gl in
let (_,xval,_) = pf_get_hyp gl x in
(* If x has a body, simply replace x with body and clear x *)
- if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
+ if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) gl else
(* x is a variable: *)
let varx = mkVar x in
(* Find a non-recursive definition for x *)
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index dd02adde1d..b7d5e1802d 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Errors
open Evar_refiner
open Tacmach
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1c9833571b..4e22044d5b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -448,7 +448,7 @@ let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
let inTransitivity : bool * constr -> obj =
declare_object {(default_object "TRANSITIVITY-STEPS") with
cache_function = cache_transitivity_lemma;
- open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
+ open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
subst_function = subst_transitivity_lemma;
classify_function = (fun o -> Substitute o) }
@@ -555,10 +555,10 @@ let subst_var_with_hole occ tid t =
let locref = ref 0 in
let rec substrec = function
| GVar (_,id) as x ->
- if id = tid
+ if id_eq id tid
then
(decr occref;
- if !occref = 0 then x
+ if Int.equal !occref 0 then x
else
(incr locref;
GHole (Loc.make_loc (!locref,0),
@@ -575,7 +575,7 @@ let subst_hole_with_term occ tc t =
let rec substrec = function
| GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) ->
decr occref;
- if !occref = 0 then tc
+ if Int.equal !occref 0 then tc
else
(incr locref;
GHole (Loc.make_loc (!locref,0),
@@ -654,7 +654,7 @@ END
exception Found of tactic
let rewrite_except h g =
- tclMAP (fun id -> if id = h then tclIDTAC else
+ tclMAP (fun id -> if id_eq id h then tclIDTAC else
tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
(Tacmach.pf_ids_of_hyps g) g
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index ec8bc5f7e3..65f0e0302e 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -74,29 +74,37 @@ let has_nodep_prod = has_nodep_prod_after 0
(* style: None = record; Some false = conjunction; Some true = strict conj *)
+let is_strict_conjunction = function
+| Some true -> true
+| _ -> false
+
+let is_lax_conjunction = function
+| Some false -> true
+| _ -> false
+
let match_with_one_constructor style onlybinary allow_rec t =
let (hdapp,args) = decompose_app t in
let res = match kind_of_term hdapp with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
- if (Array.length mip.mind_consnames = 1)
+ if Int.equal (Array.length mip.mind_consnames) 1
&& (allow_rec or not (mis_is_recursive (ind,mib,mip)))
- && (mip.mind_nrealargs = 0)
+ && (Int.equal mip.mind_nrealargs 0)
then
- if style = Some true (* strict conjunction *) then
+ if is_strict_conjunction style (* strict conjunction *) then
let ctx =
(prod_assum (snd
(decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
if
List.for_all
- (fun (_,b,c) -> b=None && isRel c && destRel c = mib.mind_nparams) ctx
+ (fun (_,b,c) -> Option.is_empty b && isRel c && Int.equal (destRel c) mib.mind_nparams) ctx
then
Some (hdapp,args)
else None
else
let ctyp = prod_applist mip.mind_nf_lc.(0) args in
let cargs = List.map pi3 ((prod_assum ctyp)) in
- if style <> Some false || has_nodep_prod ctyp then
+ if not (is_lax_conjunction style) || has_nodep_prod ctyp then
(* Record or non strict conjunction *)
Some (hdapp,List.rev cargs)
else
@@ -105,7 +113,8 @@ let match_with_one_constructor style onlybinary allow_rec t =
None
| _ -> None in
match res with
- | Some (hdapp,args) when not onlybinary || List.length args = 2 -> res
+ | Some (hdapp, args) when not onlybinary -> res
+ | Some (hdapp, [_; _]) -> res
| _ -> None
let match_with_conjunction ?(strict=false) ?(onlybinary=false) t =
@@ -139,7 +148,7 @@ let is_tuple t =
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
- | [_,None,c] -> isRel c && destRel c = (n - i)
+ | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
@@ -148,9 +157,9 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
| Ind ind ->
let car = mis_constr_nargs ind in
let (mib,mip) = Global.lookup_inductive ind in
- if Array.for_all (fun ar -> ar = 1) car
+ if Array.for_all (fun ar -> Int.equal ar 1) car
&& not (mis_is_recursive (ind,mib,mip))
- && (mip.mind_nrealargs = 0)
+ && (Int.equal mip.mind_nrealargs 0)
then
if strict then
if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
@@ -166,7 +175,8 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
None
| _ -> None in
match res with
- | Some (hdapp,args) when not onlybinary || List.length args = 2 -> res
+ | Some (hdapp,args) when not onlybinary -> res
+ | Some (hdapp,[_; _]) -> res
| _ -> None
let is_disjunction ?(strict=false) ?(onlybinary=false) t =
@@ -181,7 +191,7 @@ let match_with_empty_type t =
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
let nconstr = Array.length mip.mind_consnames in
- if nconstr = 0 then Some hdapp else None
+ if Int.equal nconstr 0 then Some hdapp else None
| _ -> None
let is_empty_type t = op2bool (match_with_empty_type t)
@@ -196,8 +206,8 @@ let match_with_unit_or_eq_type t =
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- let zero_args c = nb_prod c = mib.mind_nparams in
- if nconstr = 1 && zero_args constr_types.(0) then
+ let zero_args c = Int.equal (nb_prod c) mib.mind_nparams in
+ if Int.equal nconstr 1 && zero_args constr_types.(0) then
Some hdapp
else
None
@@ -211,7 +221,7 @@ let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
let is_unit_type t =
match match_with_conjunction t with
- | Some (_,t) when List.length t = 0 -> true
+ | Some (_,[]) -> true
| _ -> false
(* Checks if a given term is an application of an
@@ -236,20 +246,20 @@ let match_with_equation t =
let (hdapp,args) = destApp t in
match kind_of_term hdapp with
| Ind ind ->
- if IndRef ind = glob_eq then
+ if eq_gr (IndRef ind) glob_eq then
Some (build_coq_eq_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if IndRef ind = glob_identity then
+ else if eq_gr (IndRef ind) glob_identity then
Some (build_coq_identity_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if IndRef ind = glob_jmeq then
+ else if eq_gr (IndRef ind) glob_jmeq then
Some (build_coq_jmeq_data()),hdapp,
HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- if nconstr = 1 then
+ if Int.equal nconstr 1 then
if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
@@ -263,7 +273,7 @@ let match_with_equation t =
let is_inductive_equality ind =
let (mib,mip) = Global.lookup_inductive ind in
let nconstr = Array.length mip.mind_consnames in
- nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
+ Int.equal nconstr 1 && Int.equal (constructor_nrealargs (Global.env()) (ind,1)) 0
let match_with_equality_type t =
let (hdapp,args) = decompose_app t in
@@ -277,7 +287,8 @@ let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
let match_arrow_pattern t =
match matches coq_arrow_pattern t with
- | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind)
+ | [(m1,arg);(m2,mind)] ->
+ assert (id_eq m1 meta1 && id_eq m2 meta2); (arg, mind)
| _ -> anomaly "Incorrect pattern matching"
let match_with_nottype t =
@@ -311,7 +322,7 @@ let match_with_nodep_ind t =
let nodep_constr = has_nodep_prod_after mib.mind_nparams in
if Array.for_all nodep_constr mip.mind_nf_lc then
let params=
- if mip.mind_nrealargs=0 then args else
+ if Int.equal mip.mind_nrealargs 0 then args else
fst (List.chop mib.mind_nparams args) in
Some (hdapp,params,mip.mind_nrealargs)
else
@@ -325,9 +336,9 @@ let match_with_sigma_type t=
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
- if (Array.length (mib.mind_packets)=1) &&
- (mip.mind_nrealargs=0) &&
- (Array.length mip.mind_consnames=1) &&
+ if Int.equal (Array.length (mib.mind_packets)) 1 &&
+ (Int.equal mip.mind_nrealargs 0) &&
+ (Int.equal (Array.length mip.mind_consnames)1) &&
has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
(*allowing only 1 existential*)
Some (hdapp,args)
@@ -357,10 +368,10 @@ let match_eq eqn eq_pat =
let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
match matches pat eqn with
| [(m1,t);(m2,x);(m3,y)] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
+ assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3);
PolymorphicLeibnizEq (t,x,y)
| [(m1,t);(m2,x);(m3,t');(m4,x')] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4);
+ assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3 && id_eq m4 meta4);
HeterogenousEq (t,x,t',x')
| _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
@@ -401,7 +412,7 @@ open Tacmach
let match_eq_nf gls eqn eq_pat =
match pf_matches gls (Lazy.force eq_pat) eqn with
| [(m1,t);(m2,x);(m3,y)] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
+ assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3);
(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
| _ -> anomaly "match_eq: an eq pattern should match 3 terms"
@@ -421,7 +432,7 @@ let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
let match_sigma ex ex_pat =
match matches (Lazy.force ex_pat) ex with
| [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
- assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4);
+ assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3 && id_eq m4 meta4);
(a,p,car,cdr)
| _ ->
anomaly "match_sigma: a successful sigma pattern should match 4 terms"
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 81c6308842..1e2d6fa6a1 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -39,9 +39,9 @@ let check_no_metas clenv ccl =
let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m))
(collect_meta_variables ccl) in
let metas = List.map (Evd.meta_name clenv.evd) metas in
+ let opts = match metas with [_] -> " " | _ -> "s " in
errorlabstrm "inversion"
- (str ("Cannot find an instantiation for variable"^
- (if List.length metas = 1 then " " else "s ")) ++
+ (str ("Cannot find an instantiation for variable"^opts) ++
prlist_with_sep pr_comma pr_name metas
(* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *))
@@ -281,10 +281,10 @@ let generalizeRewriteIntros tac depids id gls =
let rec tclMAP_i n tacfun = function
| [] -> tclDO n (tacfun None)
| a::l ->
- if n=0 then error "Too many names."
+ if Int.equal n 0 then error "Too many names."
else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
-let remember_first_eq id x = if !x = MoveLast then x := MoveAfter id
+let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
(* invariant: ProjectAndApply is responsible for erasing the clause
which it is given as input
@@ -308,7 +308,7 @@ let projectAndApply thin id eqname names depids gls =
in
let deq_trailer id neqns =
tclTHENSEQ
- [(if names <> [] then clear [id] else tclIDTAC);
+ [(if not (List.is_empty names) then clear [id] else tclIDTAC);
(tclMAP_i neqns (fun idopt ->
tclTRY (tclTHEN
(intro_move idopt MoveLast)
@@ -316,7 +316,7 @@ let projectAndApply thin id eqname names depids gls =
(* decomposition, arbitrarily try to rewrite RL !? *)
(tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))))
names);
- (if names = [] then clear [id] else tclIDTAC)]
+ (if List.is_empty names then clear [id] else tclIDTAC)]
in
substHypIfVariable
(* If no immediate variable in the equation, try to decompose it *)
@@ -377,11 +377,13 @@ let rec get_names allow_conj (loc,pat) = match pat with
| IntroRewrite _->
error "Rewriting pattern not allowed for inversion equations."
| IntroOrAndPattern [l] ->
- if allow_conj then
- if l = [] then (None,[]) else
- let l = List.map (fun id -> Option.get (fst (get_names false id))) l in
- (Some (List.hd l), l)
- else
+ let get_name id = Option.get (fst (get_names false id)) in
+ if allow_conj then begin match l with
+ | [] -> (None, [])
+ | id :: l ->
+ let n = get_name id in
+ (Some n, n :: List.map get_name l)
+ end else
error"Nested conjunctive patterns not allowed for inversion equations."
| IntroOrAndPattern l ->
error "Disjunctive patterns not allowed for inversion equations."
@@ -432,9 +434,10 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
let tac =
if gene then rewrite_equations_gene othin neqns ba
else rewrite_equations othin neqns names ba in
- if othin = Some true (* if Inversion_clear, clear the hypothesis *) then
+ match othin with
+ | Some true (* if Inversion_clear, clear the hypothesis *) ->
tclTHEN tac (tclTRY (clear [id]))
- else
+ | _ ->
tac
@@ -453,7 +456,7 @@ let raw_inversion inv_kind id status names gl =
let (elim_predicate,neqns) =
make_inv_predicate env sigma indf realargs id status (pf_concl gl) in
let (cut_concl,case_tac) =
- if status <> NoDep & (dependent c (pf_concl gl)) then
+ if status != NoDep && (dependent c (pf_concl gl)) then
Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
case_then_using
else
diff --git a/tactics/refine.ml b/tactics/refine.ml
index de073b5c9c..3d1e4f010e 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -170,10 +170,10 @@ let rec compute_metamap env sigma c = match kind_of_term c with
(* terme de preuve incomplet *)
| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
let m1,mm1,sgp1 =
- if sgp1=[] then (c1,mm1,[])
+ if List.is_empty sgp1 then (c1,mm1,[])
else replace_by_meta env sigma th1 in
let m2,mm2,sgp2 =
- if sgp2=[] then (c2,mm2,[])
+ if List.is_empty sgp2 then (c2,mm2,[])
else replace_by_meta env' sigma th2 in
TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
end
@@ -262,7 +262,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
let ensure_products n =
let p = ref 0 in
let rec aux n gl =
- if n = 0 then tclFAIL 0 (mt()) gl
+ if Int.equal n 0 then tclFAIL 0 (mt()) gl
else
tclTHEN
(tclORELSE intro (fun gl -> incr p; introf gl))
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index bd6786a67f..d1eda3f7e2 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -165,7 +165,7 @@ let build_signature evars env m (cstrs : (types * types option) option list)
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
- if obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
+ if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
else error "build_signature: no constraint can apply on a dependent argument"
| _, obj :: _ -> anomaly "build_signature: not enough products"
| _, [] ->
@@ -332,7 +332,7 @@ let convertible env evd x y =
Reductionops.is_conv env evd x y
let refresh_hypinfo env sigma hypinfo =
- if hypinfo.abs = None then
+ if Option.is_empty hypinfo.abs then
let {l2r=l2r; c=c;cl=cl;flags=flags} = hypinfo in
match c with
| Some c ->
@@ -461,7 +461,7 @@ let arrow_morphism ta tb a b =
mkApp (Lazy.force arrow, [| a; b |]), unfold_impl
let rec decomp_pointwise n c =
- if n = 0 then c
+ if Int.equal n 0 then c
else
match kind_of_term c with
| App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) ->
@@ -495,7 +495,7 @@ let lift_cstr env sigma evars (args : constr list) c ty cstr =
| Some (ty, Some rel) -> rel
in
let rec aux env prod n =
- if n = 0 then start env prod
+ if Int.equal n 0 then start env prod
else
match kind_of_term (Reduction.whd_betadeltaiota env prod) with
| Prod (na, ty, b) ->
@@ -572,7 +572,7 @@ let resolve_subrelation env avoid car rel prf rel' res =
let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
- let first = match (Array.findi (fun _ b -> b <> None) args') with
+ let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
| None -> raise (Invalid_argument "resolve_morphism") in
let morphargs, morphobjs = Array.chop first args in
@@ -609,7 +609,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
| Some r ->
[ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs')
| None ->
- if y <> None then error "Cannot rewrite the argument of a dependent function";
+ if not (Option.is_empty y) then error "Cannot rewrite the argument of a dependent function";
x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args'
in
@@ -635,7 +635,7 @@ let apply_rule hypinfo loccs : strategy =
if not (eq_env !hypinfo.cl.env env) then
hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
let unif = unify_eqn env (goalevars evars) hypinfo t in
- if unif <> None then incr occ;
+ if not (Option.is_empty unif) then incr occ;
match unif with
| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->
begin
@@ -691,8 +691,8 @@ let fold_match ?(force=false) env sigma c =
it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx)
in
let sk =
- if sortp = InProp then
- if sortc = InProp then
+ if sortp == InProp then
+ if sortc == InProp then
if dep then case_dep_scheme_kind_from_prop
else case_scheme_kind_from_prop
else (
@@ -719,7 +719,7 @@ let fold_match ?(force=false) env sigma c =
let unfold_match env sigma sk app =
match kind_of_term app with
- | App (f', args) when f' = mkConst sk ->
+ | App (f', args) when eq_constr f' (mkConst sk) ->
let v = Environ.constant_value (Global.env ()) sk in
Reductionops.whd_beta sigma (mkApp (v, args))
| _ -> app
@@ -739,11 +739,11 @@ let subterm all flags (s : strategy) : strategy =
let args', evars', progress =
Array.fold_left
(fun (acc, evars, progress) arg ->
- if progress <> None && not all then (None :: acc, evars, progress)
+ if not (Option.is_empty progress) && not all then (None :: acc, evars, progress)
else
let res = s env avoid arg (Typing.type_of env (goalevars evars) arg) None evars in
match res with
- | Some None -> (None :: acc, evars, if progress = None then Some false else progress)
+ | Some None -> (None :: acc, evars, if Option.is_empty progress then Some false else progress)
| Some (Some r) -> (Some r :: acc, r.rew_evars, Some true)
| None -> (None :: acc, evars, progress))
([], evars, success) args
@@ -873,11 +873,11 @@ let subterm all flags (s : strategy) : strategy =
let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in
Some (Some (coerce env avoid cstr res))
| x ->
- if Array.for_all ((=) 0) ci.ci_cstr_ndecls then
+ if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in
let found, brs' = Array.fold_left
(fun (found, acc) br ->
- if found <> None then (found, fun x -> lift 1 br :: acc x)
+ if not (Option.is_empty found) then (found, fun x -> lift 1 br :: acc x)
else
match s env avoid br ty cstr evars with
| Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
@@ -1232,7 +1232,7 @@ let assert_replacing id newt tac =
let nc' =
Environ.fold_named_context
(fun _ (n, b, t as decl) nc' ->
- if n = id then (n, b, newt) :: nc'
+ if id_eq n id then (n, b, newt) :: nc'
else decl :: nc')
env ~init:[]
in
@@ -1246,8 +1246,8 @@ let assert_replacing id newt tac =
let inst =
fold_named_context
(fun _ (n, b, t) inst ->
- if n = id then ev' :: inst
- else if b = None then mkVar n :: inst else inst)
+ if id_eq n id then ev' :: inst
+ else if Option.is_empty b then mkVar n :: inst else inst)
env ~init:[]
in
let (e, args) = destEvar ev in
@@ -1524,7 +1524,7 @@ TACTIC EXTEND rewrite_strat
END
let clsubstitute o c =
- let is_tac id = match fst (fst (snd c)) with GVar (_, id') when id' = id -> true | _ -> false in
+ let is_tac id = match fst (fst (snd c)) with GVar (_, id') when id_eq id' id -> true | _ -> false in
Tacticals.onAllHypsAndConcl
(fun cl ->
match cl with
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ad62e6015f..8dcb056153 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -566,7 +566,7 @@ let rec intern_atomic lf ist x =
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_pure_tactic ist) otac,
Option.map (intern_intro_pattern lf ist) ipat,
- intern_constr_gen false (otac<>None) ist c)
+ intern_constr_gen false (not (Option.is_empty otac)) ist c)
| TacGeneralize cl ->
TacGeneralize (List.map (fun (c,na) ->
intern_constr_with_occurrences ist c,
@@ -628,10 +628,16 @@ let rec intern_atomic lf ist x =
dump_glob_red_expr r;
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
| TacChange (None,c,cl) ->
+ let is_onhyps = match cl.onhyps with
+ | None | Some [] -> true
+ | _ -> false
+ in
+ let is_onconcl = match cl.concl_occs with
+ | AllOccurrences | NoOccurrences -> true
+ | _ -> false
+ in
TacChange (None,
- (if (cl.onhyps = None or cl.onhyps = Some []) &
- (cl.concl_occs = AllOccurrences or
- cl.concl_occs = NoOccurrences)
+ (if is_onhyps && is_onconcl
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
| TacChange (Some p,c,cl) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 221f2c6f4e..0cfb4bb970 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -69,14 +69,14 @@ type value =
let dloc = Loc.ghost
let catch_error call_trace tac g =
- if call_trace = [] then tac g else try tac g with
+ if List.is_empty call_trace then tac g else try tac g with
| LtacLocated _ as e -> raise e
| Loc.Exc_located (_,LtacLocated _) as e -> raise e
| e ->
let (nrep,loc',c),tail = List.sep_last call_trace in
let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
- if tail = [] then
- let loc = if loc = dloc then loc' else loc in
+ if List.is_empty tail then
+ let loc = if Loc.is_ghost loc then loc' else loc in
raise (Loc.Exc_located(loc,e'))
else
raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
@@ -150,12 +150,12 @@ let lookup_interp_genarg id =
f
let push_trace (loc,ck) = function
- | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl
+ | (n,loc',ck')::trl when Pervasives.(=) ck ck' -> (n+1,loc,ck)::trl (** FIXME *)
| trl -> (1,loc,ck)::trl
let propagate_trace ist loc id = function
| VFun (_,lfun,it,b) ->
- let t = if it=[] then b else TacFun (it,b) in
+ let t = if List.is_empty it then b else TacFun (it,b) in
VFun (push_trace(loc,LtacVarCall (id,t)) ist.trace,lfun,it,b)
| x -> x
@@ -312,7 +312,7 @@ let constr_of_value env = function
let closed_constr_of_value env v =
let ids,c = constr_of_value env v in
- if ids <> [] then raise Not_found;
+ if not (List.is_empty ids) then raise Not_found;
c
let coerce_to_hyp env = function
@@ -444,7 +444,7 @@ let interp_fresh_id ist env l =
let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in
let id =
- if l = [] then default_fresh_id
+ if List.is_empty l then default_fresh_id
else
let s =
String.concat "" (List.map (function
@@ -491,7 +491,7 @@ let interp_type = interp_constr_gen IsType
(* Interprets an open constr *)
let interp_open_constr ccl ist =
- interp_gen (OfType ccl) ist false true false (ccl<>None)
+ interp_gen (OfType ccl) ist false true false (not (Option.is_empty ccl))
let interp_pure_open_constr ist =
interp_gen (OfType None) ist false false false false
@@ -564,7 +564,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma occl =
let interp_constr_with_occurrences_and_name_as_list =
interp_constr_in_compound_list
(fun c -> ((AllOccurrences,c),Anonymous))
- (function ((occs,c),Anonymous) when occs = AllOccurrences -> c
+ (function ((occs,c),Anonymous) when occs == AllOccurrences -> c
| _ -> raise Not_found)
(fun ist env sigma (occ_c,na) ->
let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
@@ -758,7 +758,7 @@ let loc_of_bindings = function
let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
let loc1 = loc_of_glob_constr c in
let loc2 = loc_of_bindings bl in
- let loc = if loc2 = Loc.ghost then loc1 else Loc.merge loc1 loc2 in
+ let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
sigma, (loc,cb)
@@ -866,7 +866,7 @@ let equal_instances gl (ctx',c') (ctx,c) =
(* How to compare instances? Do we want the terms to be convertible?
unifiable? Do we want the universe levels to be relevant?
(historically, conv_x is used) *)
- ctx = ctx' & pf_conv_x gl c' c
+ List.equal id_eq ctx ctx' && pf_conv_x gl c' c
(* Verifies if the matched list is coherent with respect to lcm *)
(* While non-linear matching is modulo eq_constr in matches, merge of *)
@@ -874,7 +874,7 @@ let equal_instances gl (ctx',c') (ctx,c) =
let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
let rec aux = function
| (id,c as x)::tl ->
- if List.for_all (fun (id',c') -> id'<>id or equal_instances gl c' c) lcm
+ if List.for_all (fun (id',c') -> not (id_eq id' id) || equal_instances gl c' c) lcm
then
x :: aux tl
else
@@ -931,7 +931,7 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
with
| PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
match_next_pattern (fun () ->
- let hyp = if b<>None then refresh_universes_strict hyp else hyp in
+ let hyp = if Option.is_empty b then hyp else refresh_universes_strict hyp in
match_pat lmatch hyp pat) ()
| Some patv ->
match b with
@@ -1053,7 +1053,7 @@ and interp_ltac_reference loc' mustbetac ist gl = function
sigma , if mustbetac then coerce_to_tactic loc id v else v
| ArgArg (loc,r) ->
let ids = extract_ids [] ist.lfun in
- let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in
+ let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in
let ist =
{ lfun=[]; debug=ist.debug; avoid_ids=ids;
trace = push_trace loc_info ist.trace } in
@@ -1109,13 +1109,13 @@ and interp_tacarg ist gl arg =
v
| TacDynamic(_,t) ->
let tg = (Dyn.tag t) in
- if tg = "tactic" then
+ if String.equal tg "tactic" then
let (sigma,v) = val_interp ist gl (tactic_out t ist) in
evdref := sigma;
v
- else if tg = "value" then
+ else if String.equal tg "value" then
value_out t
- else if tg = "constr" then
+ else if String.equal tg "constr" then
VConstr ([],constr_out t)
else
anomaly_loc (dloc, "Tacinterp.val_interp",
@@ -1134,7 +1134,7 @@ and interp_app loc ist gl fv largs =
|VFun(trace,olfun,([] as var),
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
let (newlfun,lvar,lval)=head_with_value (var,largs) in
- if lvar=[] then
+ if List.is_empty lvar then
let (sigma,v) =
try
catch_error trace
@@ -1146,7 +1146,7 @@ and interp_app loc ist gl fv largs =
debugging_step ist
(fun () ->
str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v);
- if lval=[] then sigma,v else interp_app loc ist gl v lval
+ if List.is_empty lval then sigma,v else interp_app loc ist gl v lval
else
project gl , VFun(trace,newlfun@olfun,lvar,body)
| _ ->
@@ -1225,7 +1225,10 @@ and interp_match_goal ist goal lz lr lmr =
match_next_pattern (fun () -> match_subterm_gen app c csr) () in
let rec apply_match_goal ist env goal nrs lex lpt =
begin
- if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
+ let () = match lex with
+ | r :: _ -> db_pattern_rule ist.debug nrs r
+ | _ -> ()
+ in
match lpt with
| (All t)::tl ->
begin
@@ -1256,7 +1259,7 @@ and interp_match_goal ist goal lz lr lmr =
| _ ->
errorlabstrm "Tacinterp.apply_match_goal"
(v 0 (str "No matching clauses for match goal" ++
- (if ist.debug=DebugOff then
+ (if ist.debug == DebugOff then
fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
else mt()) ++ str"."))
end in
@@ -1478,7 +1481,7 @@ and interp_ltac_constr ist gl e =
Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
str " has value " ++ fnl() ++
pr_constr_under_binders_env (pf_env gl) cresult);
- if fst cresult <> [] then raise Not_found;
+ if not (List.is_empty (fst cresult)) then raise Not_found;
sigma , snd cresult
with Not_found ->
errorlabstrm ""
@@ -1603,7 +1606,7 @@ and interp_atomic ist gl tac =
(tclEVARS sigma)
(h_cut c_interp)
| TacAssert (t,ipat,c) ->
- let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in
+ let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
tclTHEN
(tclEVARS sigma)
(Tactics.forward (Option.map (interp_tactic ist) t)
@@ -1618,7 +1621,7 @@ and interp_atomic ist gl tac =
(h_generalize_dep c_interp)
| TacLetTac (na,c,clp,b,eqpat) ->
let clp = interp_clause ist gl clp in
- if clp = Locusops.nowhere then
+ if Locusops.is_nowhere clp then
(* We try to fully-typecheck the term *)
let (sigma,c_interp) = pf_interp_constr ist gl c in
tclTHEN
@@ -1716,10 +1719,16 @@ and interp_atomic ist gl tac =
(tclEVARS sigma)
(h_reduce r_interp (interp_clause ist gl cl))
| TacChange (None,c,cl) ->
+ let is_onhyps = match cl.onhyps with
+ | None | Some [] -> true
+ | _ -> false
+ in
+ let is_onconcl = match cl.concl_occs with
+ | AllOccurrences | NoOccurrences -> true
+ | _ -> false
+ in
let (sigma,c_interp) =
- if (cl.onhyps = None or cl.onhyps = Some []) &
- (cl.concl_occs = AllOccurrences or
- cl.concl_occs = NoOccurrences)
+ if is_onhyps && is_onconcl
then pf_interp_type ist gl c
else pf_interp_constr ist gl c
in
@@ -1828,7 +1837,7 @@ and interp_atomic ist gl tac =
let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
evdref := sigma;
VConstr ([],c_interp)
- | ExtraArgType s when tactic_genarg_level s <> None ->
+ | ExtraArgType s when not (Option.is_empty (tactic_genarg_level s)) ->
(* Special treatment of tactic arguments *)
let (sigma,v) = val_interp ist gl
(out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 42f1424422..d5b4e31971 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -42,7 +42,7 @@ let subst_quantified_hypothesis _ x = x
let subst_declared_or_quantified_hypothesis _ x = x
let subst_glob_constr_and_expr subst (c,e) =
- assert (e=None); (* e<>None only for toplevel tactics *)
+ assert (Option.is_empty e); (* e<>None only for toplevel tactics *)
(Detyping.subst_glob_constr subst c,None)
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 20a52c21c5..68d4890fd3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -109,7 +109,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
let onNLastHyps n tac = onHyps (nLastHyps n) tac
let afterHyp id gl =
- fst (List.split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+ fst (List.split_when (fun (hyp,_,_) -> id_eq hyp id) (pf_hyps gl))
(***************************************)
(* Clause Tacticals *)
@@ -175,10 +175,12 @@ let fix_empty_or_and_pattern nv l =
names and "[ ]" for no clause at all *)
(* 2- More generally, we admit "[ ]" for any disjunctive pattern of
arbitrary length *)
- if l = [[]] then List.make nv [] else l
+ match l with
+ | [[]] -> List.make nv []
+ | _ -> l
let check_or_and_pattern_size loc names n =
- if List.length names <> n then
+ if not (Int.equal (List.length names) n) then
if Int.equal n 1 then
user_err_loc (loc,"",str "Expects a conjunctive pattern.")
else
@@ -201,7 +203,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
| Prod (_,_,c), recarg::rest ->
let b = match dest_recarg recarg with
| Norec | Imbr _ -> false
- | Mrec (_,j) -> isrec & j=k
+ | Mrec (_,j) -> isrec && Int.equal j k
in b :: (analrec c rest)
| LetIn (_,_,_,c), rest -> false :: (analrec c rest)
| _, [] -> []
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a8722ea99..3d0790564c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -201,12 +201,12 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
let redfun' = pf_reduce redfun gl in
match c with
| None ->
- if where = InHypValueOnly then
+ if where == InHypValueOnly then
errorlabstrm "" (pr_id id ++ str "has no value.");
(id,None,redfun' ty)
| Some b ->
- let b' = if where <> InHypTypeOnly then redfun' b else b in
- let ty' = if where <> InHypValueOnly then redfun' ty else ty in
+ let b' = if where != InHypTypeOnly then redfun' b else b in
+ let ty' = if where != InHypValueOnly then redfun' ty else ty in
(id,Some b',ty')
(* Possibly equip a reduction with the occurrences mentioned in an
@@ -227,11 +227,11 @@ let bind_change_occurrences occs = function
let bind_red_expr_occurrences occs nbcl redexp =
let has_at_clause = function
- | Unfold l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l
- | Pattern l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l
- | Simpl (Some (occl,_)) -> occl <> AllOccurrences
+ | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Simpl (Some (occl,_)) -> occl != AllOccurrences
| _ -> false in
- if occs = AllOccurrences then
+ if occs == AllOccurrences then
if nbcl > 1 && has_at_clause redexp then
error_illegal_non_atomic_clause ()
else
@@ -241,24 +241,24 @@ let bind_red_expr_occurrences occs nbcl redexp =
| Unfold (_::_::_) ->
error_illegal_clause ()
| Unfold [(occl,c)] ->
- if occl <> AllOccurrences then
+ if occl != AllOccurrences then
error_illegal_clause ()
else
Unfold [(occs,c)]
| Pattern (_::_::_) ->
error_illegal_clause ()
| Pattern [(occl,c)] ->
- if occl <> AllOccurrences then
+ if occl != AllOccurrences then
error_illegal_clause ()
else
Pattern [(occs,c)]
| Simpl (Some (occl,c)) ->
- if occl <> AllOccurrences then
+ if occl != AllOccurrences then
error_illegal_clause ()
else
Simpl (Some (occs,c))
| CbvVm (Some (occl,c)) ->
- if occl <> AllOccurrences then
+ if occl != AllOccurrences then
error_illegal_clause ()
else
CbvVm (Some (occs,c))
@@ -280,7 +280,7 @@ let reduct_in_hyp redfun (id,where) gl =
(pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
let revert_cast (redfun,kind as r) =
- if kind = DEFAULTcast then (redfun,REVERTcast) else r
+ if kind == DEFAULTcast then (redfun,REVERTcast) else r
let reduct_option redfun = function
| Some id -> reduct_in_hyp (fst redfun) id
@@ -401,7 +401,7 @@ let find_name loc decl gl = function
| IntroMustBe id ->
(* When name is given, we allow to hide a global name *)
let id' = next_ident_away id (pf_ids_of_hyps gl) in
- if id'<>id then user_err_loc (loc,"",pr_id id ++ str" is already used.");
+ if not (id_eq id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
id'
(* Returns the names that would be created by intros, without doing
@@ -470,7 +470,7 @@ let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
let rec get_next_hyp_position id = function
| [] -> error ("No such hypothesis: " ^ string_of_id id)
| (hyp,_,_) :: right ->
- if hyp = id then
+ if id_eq hyp id then
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
else
get_next_hyp_position id right
@@ -621,7 +621,7 @@ let apply_term hdc argl gl =
refine (applist (hdc,argl)) gl
let bring_hyps hyps =
- if hyps = [] then Refiner.tclIDTAC
+ if List.is_empty hyps then Refiner.tclIDTAC
else
(fun gl ->
let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
@@ -722,7 +722,7 @@ let last_arg c = match kind_of_term c with
| _ -> anomaly "last_arg"
let nth_arg i c =
- if i = -1 then last_arg c else
+ if Int.equal i (-1) then last_arg c else
match kind_of_term c with
| App (f,cl) -> cl.(i)
| _ -> anomaly "nth_arg"
@@ -793,7 +793,7 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl =
let general_case_analysis with_evars (c,lbindc as cx) =
match kind_of_term c with
- | Var id when lbindc = NoBindings ->
+ | Var id when lbindc == NoBindings ->
tclTHEN (try_intros_until_id_check id)
(general_case_analysis_in_context with_evars cx)
| _ ->
@@ -828,7 +828,7 @@ let elim_in_context with_evars c = function
let elim with_evars (c,lbindc as cx) elim =
match kind_of_term c with
- | Var id when lbindc = NoBindings ->
+ | Var id when lbindc == NoBindings ->
tclTHEN (try_intros_until_id_check id)
(elim_in_context with_evars cx elim)
| _ ->
@@ -973,7 +973,7 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
with Redelimination ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
- try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit
+ try if not (Int.equal concl_nprod 0) then try_apply thm_ty 0 else raise Exit
with PretypeError _|RefinerError _|UserError _|Failure _|Exit ->
if with_destruct then
descend_in_conjunctions
@@ -1022,7 +1022,7 @@ let find_matching_clause unifier clause =
let progress_with_clause flags innerclause clause =
let ordered_metas = List.rev (clenv_independent clause) in
- if ordered_metas = [] then error "Statement without assumptions.";
+ if List.is_empty ordered_metas then error "Statement without assumptions.";
let f mv =
try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause)
with Failure _ -> None
@@ -1127,7 +1127,7 @@ let (assumption : tactic) = fun gl ->
* goal. *)
let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
- if ids=[] then tclIDTAC else thin ids
+ if List.is_empty ids then tclIDTAC else thin ids
let clear_body = thin_body
@@ -1155,7 +1155,7 @@ let rec intros_clearing = function
let specialize mopt (c,lbind) g =
let tac, term =
- if lbind = NoBindings then
+ if lbind == NoBindings then
let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
tclEVARS evd, nf_evar evd c
else
@@ -1213,7 +1213,7 @@ let keep hyps gl =
let check_number_of_constructors expctdnumopt i nconstr =
if Int.equal i 0 then error "The constructors are numbered starting from 1.";
begin match expctdnumopt with
- | Some n when n <> nconstr ->
+ | Some n when not (Int.equal n nconstr) ->
error ("Not an inductive goal with "^
string_of_int n ^ String.plural n " constructor"^".")
| _ -> ()
@@ -1295,7 +1295,7 @@ let intro_or_and_pattern loc b ll l' tac id gl =
let c = mkVar id in
let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
let nv = mis_constr_nargs ind in
- let bracketed = b or not (l'=[]) in
+ let bracketed = b || not (List.is_empty l') in
let rec adjust_names_length nb n = function
| [] when Int.equal n 0 or not bracketed -> []
| [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) []
@@ -1351,13 +1351,13 @@ let wild_id = id_of_string "_tmp"
let rec list_mem_assoc_right id = function
| [] -> false
- | (x,id')::l -> id = id' || list_mem_assoc_right id l
+ | (x,id')::l -> id_eq id id' || list_mem_assoc_right id l
let check_thin_clash_then id thin avoid tac =
if list_mem_assoc_right id thin then
let newid = next_ident_away (add_suffix id "'") avoid in
let thin =
- List.map (on_snd (fun id' -> if id = id' then newid else id')) thin in
+ List.map (on_snd (fun id' -> if id_eq id id' then newid else id')) thin in
tclTHEN (rename_hyp [id,newid]) (tac thin)
else
tac thin
@@ -1441,7 +1441,7 @@ let ipat_of_name = function
let allow_replace c gl = function (* A rather arbitrary condition... *)
| Some (_, IntroIdentifier id) ->
let c = fst (decompose_app ((strip_lam_assum c))) in
- isVar c && destVar c = id
+ isVar c && id_eq (destVar c) id
| _ ->
false
@@ -1561,7 +1561,7 @@ let generalize_dep ?(with_let=false) c gl =
let cl'' = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) cl' in
let args = Array.to_list (instance_from_named_context to_quantify_rev) in
tclTHEN
- (apply_type cl'' (if body = None then c::args else args))
+ (apply_type cl'' (if Option.is_empty body then c::args else args))
(thin (List.rev tothin'))
gl
@@ -1569,7 +1569,7 @@ let generalize_gen_let lconstr gl =
let newcl =
List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
apply_type newcl (List.map_filter (fun ((_,c,b),_) ->
- if b = None then Some c else None) lconstr) gl
+ if Option.is_empty b then Some c else None) lconstr) gl
let generalize_gen lconstr =
generalize_gen_let (List.map (fun ((occs,c),na) ->
@@ -1631,7 +1631,7 @@ let out_arg = function
let occurrences_of_hyp id cls =
let rec hyp_occ = function
[] -> None
- | ((occs,id'),hl)::_ when id=id' ->
+ | ((occs,id'),hl)::_ when id_eq id id' ->
Some (occurrences_map (List.map out_arg) occs, hl)
| _::l -> hyp_occ l in
match cls.onhyps with
@@ -1639,10 +1639,10 @@ let occurrences_of_hyp id cls =
| Some l -> hyp_occ l
let occurrences_of_goal cls =
- if cls.concl_occs = NoOccurrences then None
+ if cls.concl_occs == NoOccurrences then None
else Some (occurrences_map (List.map out_arg) cls.concl_occs)
-let in_every_hyp cls = (cls.onhyps=None)
+let in_every_hyp cls = Option.is_empty cls.onhyps
(*
(* Implementation with generalisation then re-intro: introduces noise *)
@@ -1741,13 +1741,16 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
let compute_dependency _ (hyp,_,_ as d) depdecls =
match occurrences_of_hyp hyp occs with
| None -> depdecls
- | Some occ ->
+ | Some ((AllOccurrences, InHyp) as occ) ->
let newdecl = subst_closed_term_occ_decl_modulo occ test d in
- if occ = (AllOccurrences,InHyp) & eq_named_declaration d newdecl then
- if check_occs & not (in_every_hyp occs)
- then raise (RefinerError (DoesNotOccurIn (c,hyp)))
- else depdecls
+ if eq_named_declaration d newdecl then
+ if check_occs && not (in_every_hyp occs)
+ then raise (RefinerError (DoesNotOccurIn (c,hyp)))
+ else depdecls
else
+ (subst1_named_decl (mkVar id) newdecl)::depdecls
+ | Some occ ->
+ let newdecl = subst_closed_term_occ_decl_modulo occ test d in
(subst1_named_decl (mkVar id) newdecl)::depdecls in
let depdecls = fold_named_context compute_dependency env ~init:[] in
let ccl = match occurrences_of_goal occs with
@@ -1755,14 +1758,14 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
| Some occ ->
subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
let lastlhyp =
- if depdecls = [] then MoveLast else MoveAfter(pi1(List.last depdecls)) in
+ if List.is_empty depdecls then MoveLast else MoveAfter(pi1(List.last depdecls)) in
(depdecls,lastlhyp,ccl,out test)
let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
let id =
let t = match ty with Some t -> t | None -> typ_of (pf_env gl) sigmac c in
let x = id_of_name_using_hdchar (Global.env()) t name in
- if name = Anonymous then fresh_id [] x gl else
+ if name == Anonymous then fresh_id [] x gl else
if not (mem_named_context x (pf_hyps gl)) then x else
error ("The variable "^(string_of_id x)^" is already declared.") in
let (depdecls,lastlhyp,ccl,c) = letin_abstract id c test occs gl in
@@ -1838,7 +1841,7 @@ let unfold_body x gl =
let unfold_all x gl =
let (_,xval,_) = pf_get_hyp gl x in
(* If x has a body, simply replace x with body and clear x *)
- if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl
+ if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) gl
else tclIDTAC gl
(* Either unfold and clear if defined or simply clear if not a definition *)
@@ -1881,7 +1884,7 @@ let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id])
*)
let check_unused_names names =
- if names <> [] & Flags.is_verbose () then
+ if not (List.is_empty names) && Flags.is_verbose () then
msg_warning
(str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
++ str": " ++ prlist_with_sep spc pr_intro_pattern names)
@@ -2001,7 +2004,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
let params = List.firstn nparams argl in
(* le gl est important pour ne pas préévaluer *)
let rec atomize_one i avoid gl =
- if i<>nparams then
+ if not (Int.equal i nparams) then
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
(* If argl <> [], we expect typ0 not to be quantified, in order to
avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
@@ -2123,11 +2126,11 @@ let cook_sign hyp0_opt indvars env =
let lstatus = ref [] in
let before = ref true in
let seek_deps env (hyp,_,_ as decl) rhyp =
- if hyp = hyp0 then begin
+ if id_eq hyp hyp0 then begin
before:=false;
(* If there was no main induction hypotheses, then hyp is one of
indvars too, so add it to indhyps. *)
- (if hyp0_opt=None then indhyps := hyp::!indhyps);
+ (if Option.is_empty hyp0_opt then indhyps := hyp::!indhyps);
MoveFirst (* fake value *)
end else if List.mem hyp indvars then begin
(* warning: hyp can still occur after induction *)
@@ -2135,7 +2138,7 @@ let cook_sign hyp0_opt indvars env =
indhyps := hyp::!indhyps;
rhyp
end else
- if inhyps <> [] && List.mem hyp inhyps || inhyps = [] &&
+ if not (List.is_empty inhyps) && List.mem hyp inhyps || List.is_empty inhyps &&
(List.exists (fun id -> occur_var_in_decl env id decl) allindhyps ||
List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
then begin
@@ -2151,7 +2154,7 @@ let cook_sign hyp0_opt indvars env =
let _ = fold_named_context seek_deps env ~init:MoveFirst in
(* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
let compute_lstatus lhyp (hyp,_,_) =
- if hyp = hyp0 then raise (Shunt lhyp);
+ if id_eq hyp hyp0 then raise (Shunt lhyp);
if List.mem hyp !ldeps then begin
lstatus := (hyp,lhyp)::!lstatus;
lhyp
@@ -2168,7 +2171,7 @@ let cook_sign hyp0_opt indvars env =
| MoveAfter hyp -> Some hyp
| _ -> assert false in
let statuslists = (!lstatus,List.rev !rstatus) in
- let recargdests = AfterFixedPosition (if hyp0_opt=None then None else lhyp0) in
+ let recargdests = AfterFixedPosition (if Option.is_empty hyp0_opt then None else lhyp0) in
(statuslists, (recargdests,None),
!indhyps, !decldeps)
@@ -2249,7 +2252,7 @@ let make_base n id =
number, also deals with a list of names to avoid. If the inductive
type is None, then hyprecname is IHi where i is a number. *)
let make_up_names n ind_opt cname =
- let is_hyp = atompart_of_id cname = "H" in
+ let is_hyp = String.equal (atompart_of_id cname) "H" in
let base = string_of_id (make_base n cname) in
let ind_prefix = "IH" in
let base_ind =
@@ -2267,13 +2270,13 @@ let make_up_names n ind_opt cname =
let avoid =
(make_ident (string_of_id hyprecname) None) ::
(make_ident (string_of_id hyprecname) (Some 0)) :: [] in
- if atompart_of_id cname <> "H" then
+ if not (String.equal (atompart_of_id cname) "H") then
(make_ident base (Some 0)) :: (make_ident base None) :: avoid
else avoid in
id_of_string base, hyprecname, avoid
let error_ind_scheme s =
- let s = if s <> "" then s^" " else s in
+ let s = if not (String.equal s "") then s^" " else s in
error ("Cannot recognize "^s^"an induction scheme.")
let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
@@ -2401,8 +2404,9 @@ let linear vars args =
true
with Seen -> false
-let is_defined_variable env id =
- pi2 (lookup_named id env) <> None
+let is_defined_variable env id = match lookup_named id env with
+| (_, None, _) -> false
+| (_, Some _, _) -> true
let abstract_args gl generalize_vars dep id defined f args =
let sigma = project gl in
@@ -2493,7 +2497,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
let f, args = decompose_app t in
f, args, true, id, oldid
in
- if args = [] then tclIDTAC gl
+ if List.is_empty args then tclIDTAC gl
else
let args = Array.of_list args in
let newc = abstract_args gl generalize_vars force_dep id def f args in
@@ -2507,7 +2511,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
else
tclTHENLIST [refine newc; clear [id]; tclDO n intro]
in
- if vars = [] then tac gl
+ if List.is_empty vars then tac gl
else tclTHEN tac
(fun gl -> tclFIRST [revert vars ;
tclMAP (fun id ->
@@ -2711,7 +2715,7 @@ let compute_elim_sig ?elimc elimt =
| Construct _ -> true
| _ -> false in
let hi_args_enough = (* hi a le bon nbre d'arguments *)
- List.length hi_args = List.length params + !res.nargs -1 in
+ Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in
(* FIXME: Ces deux tests ne sont pas suffisants. *)
if not (hi_is_ind & hi_args_enough) then raise Exit (* No indarg *)
else (* Last arg is the indarg *)
@@ -2746,7 +2750,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
let cond hd = eq_constr hd indhd in
let check_concl is_pred p =
(* Check again conclusion *)
- let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
+ let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in
let ind_is_ok =
List.equal eq_constr
(List.lastn scheme.nargs indargs)
@@ -2768,7 +2772,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
(is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c
| LetIn (_,_,_,c) ->
(OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c
- | _ when is_pred p c = IndArg -> []
+ | _ when is_pred p c == IndArg -> []
| _ -> raise Exit
in
let rec find_branches p lbrch =
@@ -2777,12 +2781,12 @@ let compute_scheme_signature scheme names_info ind_type_guess =
(try
let lchck_brch = check_branch p t in
let n = List.fold_left
- (fun n (b,_) -> if b=RecArg then n+1 else n) 0 lchck_brch in
+ (fun n (b,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
let recvarname, hyprecname, avoid =
make_up_names n scheme.indref names_info in
let namesign =
List.map (fun (b,dep) ->
- (b,dep,if b=IndArg then hyprecname else recvarname))
+ (b, dep, if b == IndArg then hyprecname else recvarname))
lchck_brch in
(avoid,namesign) :: find_branches (p+1) brs
with Exit-> error_ind_scheme "the branches of")
@@ -2846,7 +2850,7 @@ let find_induction_type isrec elim hyp0 gl =
| Some e ->
let (elimc,elimt),ind_guess = given_elim hyp0 e gl in
let scheme = compute_elim_sig ~elimc elimt in
- if scheme.indarg = None then error "Cannot find induction type";
+ if Option.is_empty scheme.indarg then error "Cannot find induction type";
let indsign = compute_scheme_signature scheme hyp0 ind_guess in
let elim = ({elimindex = Some(-1); elimbody = elimc},elimt) in
scheme, ElimUsing (elim,indsign) in
@@ -2861,7 +2865,7 @@ let is_functional_induction elim gl =
let scheme = compute_elim_sig ~elimc (pf_type_of gl (fst elimc)) in
(* The test is not safe: with non-functional induction on non-standard
induction scheme, this may fail *)
- scheme.indarg = None
+ Option.is_empty scheme.indarg
| None ->
false
@@ -2953,11 +2957,11 @@ let apply_induction_in_context hyp0 elim indvars names induct_tac gl =
let dephyps = List.map (fun (id,_,_) -> id) deps in
let deps_cstr =
List.fold_left
- (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in
+ (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
tclTHENLIST
[
(* Generalize dependent hyps (but not args) *)
- if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr;
+ if List.is_empty deps then tclIDTAC else apply_type tmpcl deps_cstr;
(* clear dependent hyps *)
thin dephyps;
(* side-conditions in elim (resp case) schemes come last (resp first) *)
@@ -2978,9 +2982,9 @@ let induction_from_context_l with_evars elim_info lid names gl =
(* number of all args, counting farg and indarg if present. *)
let nargs_indarg_farg = scheme.nargs
+ (if scheme.farg_in_concl then 1 else 0)
- + (if scheme.indarg <> None then 1 else 0) in
+ + (if Option.is_empty scheme.indarg then 0 else 1) in
(* Number of given induction args must be exact. *)
- if List.length lid <> nargs_indarg_farg + scheme.nparams then
+ if not (Int.equal (List.length lid) (nargs_indarg_farg + scheme.nparams)) then
error "Not the right number of arguments given to induction scheme.";
(* hyp0 is used for re-introducing hyps at the right place afterward.
We chose the first element of the list of variables on which to
@@ -2995,7 +2999,7 @@ let induction_from_context_l with_evars elim_info lid names gl =
e, ivs, lp in
(* terms to patternify we must patternify indarg or farg if present in concl *)
let lid_in_pattern =
- if scheme.indarg <> None & not scheme.indarg_in_concl then List.rev indvars
+ if not (Option.is_empty scheme.indarg) && not scheme.indarg_in_concl then List.rev indvars
else List.rev (hyp0::indvars) in
let lidcstr = List.map (fun x -> mkVar x) lid_in_pattern in
let realindvars = (* hyp0 is a real induction arg if it is not the
@@ -3054,19 +3058,19 @@ let induction_without_atomization isrec with_evars elim names lid gl =
let awaited_nargs =
scheme.nparams + scheme.nargs
+ (if scheme.farg_in_concl then 1 else 0)
- + (if scheme.indarg <> None then 1 else 0)
+ + (if Option.is_empty scheme.indarg then 0 else 1)
in
let nlid = List.length lid in
- if nlid <> awaited_nargs
+ if not (Int.equal nlid awaited_nargs)
then error "Not the right number of induction arguments."
else induction_from_context_l with_evars elim_info lid names gl
let has_selected_occurrences = function
| None -> false
| Some cls ->
- cls.concl_occs <> AllOccurrences ||
- cls.onhyps <> None && List.exists (fun ((occs,_),hl) ->
- occs <> AllOccurrences || hl <> InHyp) (Option.get cls.onhyps)
+ cls.concl_occs != AllOccurrences ||
+ not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) ->
+ occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps)
(* assume that no occurrences are selected *)
let clear_unselected_context id inhyps cls gl =
@@ -3074,7 +3078,7 @@ let clear_unselected_context id inhyps cls gl =
| None -> tclIDTAC gl
| Some cls ->
if occur_var (pf_env gl) id (pf_concl gl) &&
- cls.concl_occs = NoOccurrences
+ cls.concl_occs == NoOccurrences
then errorlabstrm ""
(str "Conclusion must be mentioned: it depends on " ++ pr_id id
++ str ".");
@@ -3096,8 +3100,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls gl
| _ -> [] in
match kind_of_term c with
| Var id when not (mem_named_context id (Global.named_context()))
- & lbind = NoBindings & not with_evars & eqname = None
- & not (has_selected_occurrences cls) ->
+ && lbind == NoBindings && not with_evars && Option.is_empty eqname
+ && not (has_selected_occurrences cls) ->
tclTHEN
(clear_unselected_context id inhyps cls)
(induction_with_atomization_of_ind_arg
@@ -3123,7 +3127,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls gl
(mandatory for the moment), so we don't need to deal with
parameters of the inductive type as in new_induct_gen. *)
let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
- if eqname <> None then
+ if not (Option.is_empty eqname) then
errorlabstrm "" (str "Do not know what to do with " ++
pr_intro_pattern (Option.get eqname));
let newlc = ref [] in
@@ -3176,11 +3180,11 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
else begin
(* functional induction *)
(* Several induction hyps: induction scheme is mandatory *)
- if elim = None
+ if Option.is_empty elim
then
errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypotheses are given.\n" ++
str "Example: induction x1 x2 x3 using my_scheme.");
- if cls <> None then
+ if not (Option.is_empty cls) then
error "'in' clause not supported here.";
let lc = List.map
(map_induction_arg (pf_apply finish_evar_resolution gl)) lc in
@@ -3190,7 +3194,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl =
(* will be removable when is_functional_induction will be more clever *)
onInductionArg
(fun (c,lbind) ->
- if lbind <> NoBindings then
+ if lbind != NoBindings then
error "'with' clause not supported here.";
new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl
| _ ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index afd0e77999..5b41e0b3be 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -106,7 +106,7 @@ let bugged_is_binary t =
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
- mib.Declarations.mind_nparams = 2
+ Int.equal mib.Declarations.mind_nparams 2
| _ -> false
let iter_tac tacl =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 10:20:29 +0000