aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorppedrot2012-11-22 18:09:55 +0000
committerppedrot2012-11-22 18:09:55 +0000
commite363a1929d9a57643ac4b947cfafbb65bfd878cd (patch)
treef319f1e118b2481b38986c1ed531677ed428edca
parent2e43b03b0bb88bd3b4cb7695d5079c51ca41b0a7 (diff)
Monomorphization (pretyping)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--pretyping/cases.ml196
-rw-r--r--pretyping/cbv.ml4
-rw-r--r--pretyping/classops.ml37
-rw-r--r--pretyping/coercion.ml20
-rw-r--r--pretyping/detyping.ml54
-rw-r--r--pretyping/evarconv.ml59
-rw-r--r--pretyping/evarutil.ml108
-rw-r--r--pretyping/evd.ml93
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/glob_ops.ml28
-rw-r--r--pretyping/indrec.ml19
-rw-r--r--pretyping/inductiveops.ml17
-rw-r--r--pretyping/matching.ml14
-rw-r--r--pretyping/namegen.ml25
-rw-r--r--pretyping/patternops.ml12
-rw-r--r--pretyping/pretyping.ml34
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/reductionops.ml29
-rw-r--r--pretyping/retyping.ml11
-rw-r--r--pretyping/tacred.ml56
-rw-r--r--pretyping/term_dnet.ml8
-rw-r--r--pretyping/termops.ml57
-rw-r--r--pretyping/termops.mli2
-rw-r--r--pretyping/typeclasses.ml34
-rw-r--r--pretyping/typing.ml4
-rw-r--r--pretyping/unification.ml56
26 files changed, 579 insertions, 403 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e7300fceaf..ab9ed29935 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -94,10 +94,10 @@ let make_anonymous_patvars n =
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
-let relocate_rel n1 n2 k j = if j = n1+k then n2+k else j
+let relocate_rel n1 n2 k j = if Int.equal j (n1 + k) then n2+k else j
let rec relocate_index n1 n2 k t = match kind_of_term t with
- | Rel j when j = n1+k -> mkRel (n2+k)
+ | Rel j when Int.equal j (n1 + k) -> mkRel (n2+k)
| Rel j when j < n1+k -> t
| Rel j when j > n1+k -> t
| _ -> map_constr_with_binders succ (relocate_index n1 n2) k t
@@ -300,12 +300,15 @@ let binding_vars_of_inductive = function
| IsInd (_,IndType(_,realargs),_) -> List.filter isRel realargs
let extract_inductive_data env sigma (_,b,t) =
- if b<>None then (NotInd (None,t),[]) else
- let tmtyp =
- try try_find_ind env sigma t None
- with Not_found -> NotInd (None,t) in
- let tmtypvars = binding_vars_of_inductive tmtyp in
- (tmtyp,tmtypvars)
+ match b with
+ | None ->
+ let tmtyp =
+ try try_find_ind env sigma t None
+ with Not_found -> NotInd (None,t) in
+ let tmtypvars = binding_vars_of_inductive tmtyp in
+ (tmtyp,tmtypvars)
+ | Some _ ->
+ (NotInd (None, t), [])
let unify_tomatch_with_patterns evdref env loc typ pats realnames =
match find_row_ind pats with
@@ -372,7 +375,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
| Some (_,(ind,_)) ->
let indt = inductive_template pb.evdref pb.env None ind in
let current =
- if deps = [] & isEvar typ then
+ if List.is_empty deps && isEvar typ then
(* Don't insert coercions if dependent; only solve evars *)
let _ = e_cumul pb.env pb.evdref indt typ in
current
@@ -448,7 +451,7 @@ let check_and_adjust_constructor env ind cstrs = function
(* Check the constructor has the right number of args *)
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
- if List.length args = nb_args_constr then pat
+ if Int.equal (List.length args) nb_args_constr then pat
else
try
let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
@@ -501,11 +504,11 @@ let mk_dep_patt_row (pats,_,eqn) =
List.map (is_dep_patt_in eqn) pats
let dependencies_in_pure_rhs nargs eqns =
- if eqns = [] && not (Flags.is_program_mode ()) then
+ if List.is_empty eqns && not (Flags.is_program_mode ()) then
List.make nargs false (* Only "_" patts *) else
let deps_rows = List.map mk_dep_patt_row eqns in
let deps_columns = matrix_transpose deps_rows in
- List.map (List.exists ((=) true)) deps_columns
+ List.map (List.exists (fun x -> x)) deps_columns
let dependent_decl a = function
| (na,None,t) -> dependent a t
@@ -543,7 +546,7 @@ let rec find_dependency_list tmblock = function
let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
let deps = find_dependency_list (tm::tmtypleaves) nextlist in
- if is_dep_or_cstr_in_rhs || deps <> []
+ if is_dep_or_cstr_in_rhs || not (List.is_empty deps)
then ((true ,deps,d)::nextlist)
else ((false,[] ,d)::nextlist)
@@ -585,12 +588,17 @@ let relocate_index_tomatch n1 n2 =
(* [replace_tomatch n c tomatch] replaces [Rel n] by [c] in [tomatch] *)
let rec replace_term n c k t =
- if isRel t && destRel t = n+k then lift k c
+ if isRel t && Int.equal (destRel t) (n + k) then lift k c
else map_constr_with_binders succ (replace_term n c) k t
-let length_of_tomatch_type_sign na = function
- | NotInd _ -> if na<>Anonymous then 1 else 0
- | IsInd (_,_,names) -> List.length names + if na<>Anonymous then 1 else 0
+let length_of_tomatch_type_sign na t =
+ let l = match na with
+ | Anonymous -> 0
+ | Name _ -> 1
+ in
+ match t with
+ | NotInd _ -> l
+ | IsInd (_, _, names) -> List.length names + l
let replace_tomatch n c =
let rec replrec depth = function
@@ -598,7 +606,7 @@ let replace_tomatch n c =
| Pushed ((b,tm),l,na) :: rest ->
let b = replace_term n c depth b in
let tm = map_tomatch_type (replace_term n c depth) tm in
- List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l;
+ List.iter (fun i -> if Int.equal i (n + depth) then anomaly "replace_tomatch") l;
Pushed ((b,tm),l,na) :: replrec depth rest
| Alias (na,b,d) :: rest ->
(* [b] is out of replacement scope *)
@@ -805,10 +813,14 @@ let subst_predicate (args,copt) ccl tms =
substnl_predicate sigma 0 ccl tms
let specialize_predicate_var (cur,typ,dep) tms ccl =
- let c = if dep<>Anonymous then Some cur else None in
+ let c = match dep with
+ | Anonymous -> None
+ | Name _ -> Some cur
+ in
let l =
match typ with
- | IsInd (_,IndType(_,realargs),names) -> if names<>[] then realargs else []
+ | IsInd (_, IndType (_, _), []) -> []
+ | IsInd (_, IndType (_, realargs), names) -> realargs
| NotInd _ -> [] in
subst_predicate (l,c) ccl tms
@@ -822,7 +834,9 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
(* then we have to replace x by x' in t(x) and y by y' in P *)
(*****************************************************************************)
let generalize_predicate (names,na) ny d tms ccl =
- if na=Anonymous then anomaly "Undetected dependency";
+ let () = match na with
+ | Anonymous -> anomaly "Undetected dependency"
+ | _ -> () in
let p = List.length names + 1 in
let ccl = lift_predicate 1 ccl tms in
regeneralize_index_predicate (ny+p+1) ccl tms
@@ -847,15 +861,22 @@ let rec extract_predicate ccl = function
| Abstract (i,d)::tms ->
mkProd_wo_LetIn d (extract_predicate ccl tms)
| Pushed ((cur,NotInd _),_,na)::tms ->
- let tms = if na<>Anonymous then lift_tomatch_stack 1 tms else tms in
- let pred = extract_predicate ccl tms in
- if na<>Anonymous then subst1 cur pred else pred
+ begin match na with
+ | Anonymous -> extract_predicate ccl tms
+ | Name _ ->
+ let tms = lift_tomatch_stack 1 tms in
+ let pred = extract_predicate ccl tms in
+ subst1 cur pred
+ end
| Pushed ((cur,IsInd (_,IndType(_,realargs),_)),_,na)::tms ->
let realargs = List.rev realargs in
- let k = if na<>Anonymous then 1 else 0 in
+ let k, nrealargs = match na with
+ | Anonymous -> 0, realargs
+ | Name _ -> 1, (cur :: realargs)
+ in
let tms = lift_tomatch_stack (List.length realargs + k) tms in
let pred = extract_predicate ccl tms in
- substl (if na<>Anonymous then cur::realargs else realargs) pred
+ substl nrealargs pred
| [] ->
ccl
@@ -874,7 +895,10 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
(* Pred is already dependent in the current term to match (if *)
(* (na<>Anonymous) and its realargs; we just need to adjust it to *)
(* full sign if dep in cur is not taken into account *)
- let ccl = if na <> Anonymous then ccl else lift_predicate 1 ccl tms in
+ let ccl = match na with
+ | Anonymous -> lift_predicate 1 ccl tms
+ | Name _ -> ccl
+ in
let pred = extract_predicate ccl tms in
(* Build the predicate properly speaking *)
let sign = List.map2 set_declaration_name (na::names) sign in
@@ -891,9 +915,10 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
(p+k,liftn_predicate (k-1) (p+1) ccl tms)
let adjust_impossible_cases pb pred tomatch submat =
- if submat = [] then
- match kind_of_term (whd_evar !(pb.evdref) pred) with
- | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) = Evar_kinds.ImpossibleCase ->
+ match submat with
+ | [] ->
+ begin match kind_of_term (whd_evar !(pb.evdref) pred) with
+ | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
let default = (coq_unit_judge ()).uj_type in
pb.evdref := Evd.define evk default !(pb.evdref);
(* we add an "assert false" case *)
@@ -911,7 +936,8 @@ let adjust_impossible_cases pb pred tomatch submat =
used = ref false } ]
| _ ->
submat
- else
+ end
+ | _ ->
submat
(*****************************************************************************)
@@ -941,7 +967,8 @@ let adjust_impossible_cases pb pred tomatch submat =
let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
(* Assume some gamma st: gamma |- PI [X,x:I(X)]. PI tms. ccl *)
let nrealargs = List.length names in
- let k = nrealargs + (if depna<>Anonymous then 1 else 0) in
+ let l = match depna with Anonymous -> 0 | Name _ -> 1 in
+ let k = nrealargs + l in
(* We adjust pred st: gamma, x1..xn |- PI [X,x:I(X)]. PI tms. ccl' *)
(* so that x can later be instantiated by Ci(x1..xn) *)
(* and X by the realargs for Ci *)
@@ -949,12 +976,14 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
let ccl' = liftn_predicate n (k+1) ccl tms in
(* We prepare the substitution of X and x:I(X) *)
let realargsi =
- if nrealargs <> 0 then
+ if not (Int.equal nrealargs 0) then
adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs)
else
[] in
- let copti =
- if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
+ let copti = match depna with
+ | Anonymous -> None
+ | Name _ -> Some (build_dependent_constructor cs)
+ in
(* The substituends realargsi, copti are all defined in gamma, x1...xn *)
(* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *)
(* Note: applying the substitution in tms is not important (is it sure?) *)
@@ -976,7 +1005,10 @@ let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb =
let ((_,oldtyp),deps,na) = tomatch in
match typ, oldtyp with
| IsInd (_,_,names), NotInd _ ->
- let k = if na <> Anonymous then 2 else 1 in
+ let k = match na with
+ | Anonymous -> 1
+ | Name _ -> 2
+ in
let n = List.length names in
{ pb with pred = liftn_predicate n k pb.pred pb.tomatch },
(ct,List.map (fun i -> if i >= k then i+n else i) deps,na)
@@ -1021,10 +1053,14 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
| [], _ -> brs,tomatch,pred,[]
| n::deps, Abstract (i,d) :: tomatch ->
let d = map_rel_declaration (nf_evar evd) d in
- if List.exists (fun c -> dependent_decl (lift k c) d) tocheck || pi2 d <> None then
+ let is_d = match d with (_, None, _) -> false | _ -> true in
+ if List.exists (fun c -> dependent_decl (lift k c) d) tocheck || is_d then
(* Dependency in the current term to match and its dependencies is real *)
let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in
- let inst = if pi2 d = None then mkRel n::inst else inst in
+ let inst = match d with
+ | (_, None, _) -> mkRel n :: inst
+ | _ -> inst
+ in
brs, Abstract (i,d) :: tomatch, pred, inst
else
(* Finally, no dependency remains, so, we can replace the generalized *)
@@ -1085,14 +1121,17 @@ let rec generalize_problem names pb = function
| i::l ->
let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
let pb',deps = generalize_problem names pb l in
- if na = Anonymous & b <> None then pb',deps else
- let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *)
- let tomatch = lift_tomatch_stack 1 pb'.tomatch in
- let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
- { pb' with
- tomatch = Abstract (i,d) :: tomatch;
- pred = generalize_predicate names i d pb'.tomatch pb'.pred },
- i::deps
+ begin match (na, b) with
+ | Anonymous, Some _ -> pb', deps
+ | _ ->
+ let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *)
+ let tomatch = lift_tomatch_stack 1 pb'.tomatch in
+ let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
+ { pb' with
+ tomatch = Abstract (i,d) :: tomatch;
+ pred = generalize_predicate names i d pb'.tomatch pb'.pred },
+ i::deps
+ end
(* No more patterns: typing the right-hand side of equations *)
let build_leaf pb =
@@ -1160,10 +1199,11 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
let typs' =
List.map2
(fun (tm,(tmtyp,_),(na,_,_)) deps ->
- let na = match curname with
- | Name _ -> (if na <> Anonymous then na else curname)
- | Anonymous ->
- if deps = [] && pred_is_not_dep then Anonymous else force_name na in
+ let na = match curname, na with
+ | Name _, Anonymous -> curname
+ | Name _, Name _ -> na
+ | Anonymous, _ ->
+ if List.is_empty deps && pred_is_not_dep then Anonymous else force_name na in
((tm,tmtyp),deps,na))
typs' (List.rev dep_sign) in
@@ -1173,10 +1213,10 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
let currents = List.map (fun x -> Pushed x) typs' in
- let alias =
- if aliasname = Anonymous then
+ let alias = match aliasname with
+ | Anonymous ->
NonDepAlias
- else
+ | Name _ ->
let cur_alias = lift const_info.cs_nargs current in
let ind =
appvect (
@@ -1188,9 +1228,12 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
let tomatch = List.rev_append (alias :: currents) tomatch in
let submat = adjust_impossible_cases pb pred tomatch submat in
- if submat = [] then
+ let () = match submat with
+ | [] ->
raise_pattern_matching_error
- (Loc.ghost, pb.env, NonExhaustive (complete_history history));
+ (Loc.ghost, pb.env, NonExhaustive (complete_history history))
+ | _ -> ()
+ in
typs,
{ pb with
@@ -1235,7 +1278,8 @@ and match_current pb tomatch =
let cstrs = get_constructors pb.env indf in
let arsign, _ = get_arity pb.env indf in
let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
- if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then
+ let no_cstr = Int.equal (Array.length cstrs) 0 in
+ if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
shift_problem tomatch pb
else
(* We generalize over terms depending on current term to match *)
@@ -1447,7 +1491,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
convertible subterms of the substitution *)
let rec aux (k,env,subst as x) t =
let t = whd_evar !evdref t in match kind_of_term t with
- | Rel n when pi2 (lookup_rel n env) <> None ->
+ | Rel n when pi2 (lookup_rel n env) != None ->
map_constr_with_full_binders push_binder aux x t
| Evar ev ->
let ty = get_type_of env sigma t in
@@ -1461,8 +1505,10 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
ev
| _ ->
let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in
- if good <> [] then
- let u = pi3 (List.hd good) in (* u is in extenv *)
+ match good with
+ | [] ->
+ map_constr_with_full_binders push_binder aux x t
+ | (_, _, u) :: _ -> (* u is in extenv *)
let vl = List.map pi1 good in
let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
let depvl = free_rels ty in
@@ -1482,8 +1528,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
e_new_evar evdref extenv ~src:(loc, Evar_kinds.CasesType)
~filter ~candidates ty in
lift k ev
- else
- map_constr_with_full_binders push_binder aux x t in
+ in
aux (0,extenv,subst0) t0
let build_tycon loc env tycon_env subst tycon extenv evdref t =
@@ -1571,7 +1616,7 @@ let build_inversion_problem loc env sigma tms t =
let sub_tms =
List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
- let na = if deps = [] then Anonymous else force_name na in
+ let na = if List.is_empty deps then Anonymous else force_name na in
Pushed ((tm,tmtyp),deps,na))
dep_sign decls in
let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
@@ -1649,9 +1694,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let realnal =
match t with
| Some (loc,ind',realnal) ->
- if ind <> ind' then
+ if not (eq_ind ind ind') then
user_err_loc (loc,"",str "Wrong inductive type.");
- if nrealargs_ctxt <> List.length realnal then
+ if not (Int.equal nrealargs_ctxt (List.length realnal)) then
anomaly "Ill-formed 'in' clause in cases";
List.rev realnal
| None -> List.make nrealargs_ctxt Anonymous in
@@ -1833,11 +1878,11 @@ let constr_of_pat env isevars arsign pat avoid =
{uj_val = ty; uj_type = Typing.type_of env !isevars ty}
in
let ind, params = dest_ind_family indf in
- if ind <> cind then error_bad_constructor_loc l cstr ind;
+ if not (eq_ind ind cind) then error_bad_constructor_loc l cstr ind;
let cstrs = get_constructors env indf in
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
- assert(nb_args_constr = List.length args);
+ assert (Int.equal nb_args_constr (List.length args));
let patargs, args, sign, env, n, m, avoid =
List.fold_right2
(fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) ->
@@ -1891,17 +1936,22 @@ let eq_id avoid id =
avoid := hid' :: !avoid;
hid'
-let rels_of_patsign =
+let is_topvar t =
+match kind_of_term t with
+| Rel 0 -> true
+| _ -> false
+
+let rels_of_patsign l =
List.map (fun ((na, b, t) as x) ->
match b with
- | Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
- | _ -> x)
+ | Some t' when is_topvar t' -> (na, None, t)
+ | _ -> x) l
let vars_of_ctx ctx =
let _, y =
List.fold_right (fun (na, b, t) (prev, vars) ->
match b with
- | Some t' when kind_of_term t' = Rel 0 ->
+ | Some t' when is_topvar t' ->
prev,
(GApp (Loc.ghost,
(GRef (Loc.ghost, delayed_force coq_eq_refl_ref)),
@@ -1918,7 +1968,7 @@ let rec is_included x y =
| PatVar _, _ -> true
| _, PatVar _ -> true
| PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') ->
- if i = i' then List.for_all2 is_included args args'
+ if Int.equal i i' then List.for_all2 is_included args args'
else false
(* liftsign is the current pattern's complete signature length.
@@ -2222,7 +2272,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
constrs_of_pats typing_fun env evdref matx tomatchs sign neqs arity
in
let matx = List.rev matx in
- let _ = assert(len = List.length lets) in
+ let _ = assert (Int.equal len (List.length lets)) in
let env = push_rel_context lets env in
let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
@@ -2281,7 +2331,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
(* Main entry of the matching compilation *)
let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
- if predopt = None && Flags.is_program_mode () then
+ if predopt == None && Flags.is_program_mode () then
compile_program_cases loc style (typing_fun, evdref)
tycon env (predopt, tomatchl, eqns)
else
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 099a2ab76f..cb71e1aa6a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -85,7 +85,7 @@ let rec shift_value n = function
| CONSTR (c,args) ->
CONSTR (c, Array.map (shift_value n) args)
let shift_value n v =
- if n = 0 then v else shift_value n v
+ if Int.equal n 0 then v else shift_value n v
(* Contracts a fixpoint: given a fixpoint and a bindings,
* returns the corresponding fixpoint body, and the bindings in which
@@ -110,7 +110,7 @@ let make_constr_ref n = function
(* Adds an application list. Collapse APPs! *)
let stack_app appl stack =
- if Array.length appl = 0 then stack else
+ if Int.equal (Array.length appl) 0 then stack else
match stack with
| APP(args,stk) -> APP(Array.append appl args,stk)
| _ -> APP(appl, stack)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 52ec8d1d11..2f47074060 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -49,9 +49,9 @@ type coe_info_typ = {
let coe_info_typ_equal c1 c2 =
eq_constr c1.coe_value c2.coe_value &&
eq_constr c1.coe_type c2.coe_type &&
- c1.coe_strength = c2.coe_strength &&
- c1.coe_is_identity = c2.coe_is_identity &&
- c1.coe_param = c2.coe_param
+ c1.coe_strength == c2.coe_strength &&
+ c1.coe_is_identity == c2.coe_is_identity &&
+ Int.equal c1.coe_param c2.coe_param
type cl_index = int
@@ -69,7 +69,7 @@ module Bijint = struct
let revmap y b = let n = Gmap.find y b.inv in (n, snd (b.v.(n)))
let add x y b =
let v =
- if b.s = Array.length b.v then
+ if Int.equal b.s (Array.length b.v) then
(let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
else b.v in
v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv }
@@ -183,7 +183,7 @@ let class_of env sigma t =
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, args)
in
- if List.length args = n1 then t, i else raise Not_found
+ if Int.equal (List.length args) n1 then t, i else raise Not_found
let inductive_class_of ind = fst (class_info (CL_IND ind))
@@ -218,14 +218,14 @@ let apply_on_class_of env sigma t cont =
try
let (cl,args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
- if List.length args <> n1 then raise Not_found;
+ if not (Int.equal (List.length args) n1) then raise Not_found;
t, cont i
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
let t = Tacred.hnf_constr env sigma t in
let (cl, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
- if List.length args <> n1 then raise Not_found;
+ if not (Int.equal (List.length args) n1) then raise Not_found;
t, cont i
let lookup_path_between env sigma (s,t) =
@@ -287,7 +287,7 @@ let add_coercion_in_graph (ic,source,target) =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
let try_add_new_path (i,j as ij) p =
try
- if i=j then begin
+ if Int.equal i j then begin
if different_class_params i j then begin
let _ = lookup_path_between_class ij in
ambig_paths := (ij,p)::!ambig_paths
@@ -308,20 +308,21 @@ let add_coercion_in_graph (ic,source,target) =
if try_add_new_path (source,target) [ic] then begin
Gmap.iter
(fun (s,t) p ->
- if s<>t then begin
- if t = source then begin
+ if not (Int.equal s t) then begin
+ if Int.equal t source then begin
try_add_new_path1 (s,target) (p@[ic]);
Gmap.iter
(fun (u,v) q ->
- if u<>v & u = target && not (List.equal coe_info_typ_equal p q) then
+ if not (Int.equal u v) && Int.equal u target && not (List.equal coe_info_typ_equal p q) then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
- if s = target then try_add_new_path1 (source,t) (ic::p)
+ if Int.equal s target then try_add_new_path1 (source,t) (ic::p)
end)
old_inheritance_graph
end;
- if (!ambig_paths <> []) && is_verbose () then
+ let is_ambig = match !ambig_paths with [] -> false | _ -> true in
+ if is_ambig && is_verbose () then
msg_warning (message_ambig !ambig_paths)
type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int
@@ -376,7 +377,7 @@ let load_coercion _ o =
cache_coercion o
let open_coercion i o =
- if i = 1 && not
+ if Int.equal i 1 && not
(!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
then
cache_coercion o
@@ -394,7 +395,9 @@ let discharge_cl = function
| cl -> cl
let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
- if stre = Local then None else
+ match stre with
+ | Local -> None
+ | Global ->
let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in
Some (Lib.discharge_global coe,
stre,
@@ -404,7 +407,9 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
n + ps)
let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
- if stre = Local then Dispose else Substitute obj
+ match stre with
+ | Local -> Dispose
+ | Global -> Substitute obj
let inCoercion : coercion -> obj =
declare_object {(default_object "COERCION") with
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0239a7e44d..ff4d2837b4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,7 +79,7 @@ let disc_subset x =
Ind i ->
let len = Array.length l in
let sigty = delayed_force sig_typ in
- if len = 2 && i = Term.destInd sigty
+ if Int.equal len 2 && eq_ind i (Term.destInd sigty)
then
let (a, b) = pair_of_array l in
Some (a, b)
@@ -169,9 +169,9 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
match (kind_of_term x, kind_of_term y) with
| Sort s, Sort s' ->
(match s, s' with
- Prop x, Prop y when x = y -> None
+ Prop x, Prop y when x == y -> None
| Prop _, Type _ -> None
- | Type x, Type y when x = y -> None (* false *)
+ | Type x, Type y when Pervasives.(=) x y -> None (* false *) (** FIXME **)
| _ -> subco ())
| Prod (name, a, b), Prod (name', a', b') ->
let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
@@ -198,10 +198,10 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
let sigT = delayed_force sigT_typ in
let prod = delayed_force prod_typ in
(* Sigma types *)
- if len = Array.length l' && len = 2 && i = i'
- && (i = Term.destInd sigT || i = Term.destInd prod)
+ if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
+ && (eq_ind i (Term.destInd sigT) || eq_ind i (Term.destInd prod))
then
- if i = Term.destInd sigT
+ if eq_ind i (Term.destInd sigT)
then
begin
let (a, pb), (a', pb') =
@@ -261,8 +261,8 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
mkApp (delayed_force prod_intro, [| a'; b'; x ; y |]))
end
else
- if i = i' && len = Array.length l' then
- let evm = !isevars in
+ if eq_ind i i' && Int.equal len (Array.length l') then
+ let evm = !isevars in
(try subco ()
with NoSubtacCoercion ->
let typ = Typing.type_of env evm c in
@@ -272,8 +272,8 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
(* else subco () *)
else
subco ()
- | x, y when x = y ->
- if Array.length l = Array.length l' then
+ | x, y when Pervasives.(=) x y -> (** FIXME *)
+ if Int.equal (Array.length l) (Array.length l') then
let evm = !isevars in
let lam_type = Typing.type_of env evm c in
let lam_type' = Typing.type_of env evm c' in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ce84e6bd5e..a96deca06a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -42,9 +42,9 @@ let encode_inductive r =
(* Tables for Cases printing under a "if" form, a "let" form, *)
let has_two_constructors lc =
- Array.length lc = 2 (* & lc.(0) = 0 & lc.(1) = 0 *)
+ Int.equal (Array.length lc) 2 (* & lc.(0) = 0 & lc.(1) = 0 *)
-let isomorphic_to_tuple lc = (Array.length lc = 1)
+let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
let encode_bool r =
let (x,lc) = encode_inductive r in
@@ -167,7 +167,7 @@ let computable p k =
engendrera un prédicat non dépendant) *)
let sign,ccl = decompose_lam_assum p in
- (rel_context_length sign = k+1)
+ Int.equal (rel_context_length sign) (k + 1)
&&
noccur_between 1 (k+1) ccl
@@ -175,11 +175,11 @@ let lookup_name_as_displayed env t s =
let rec lookup avoid n c = match kind_of_term c with
| Prod (name,_,c') ->
(match compute_displayed_name_in RenamingForGoal avoid name c' with
- | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+ | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| LetIn (name,_,_,c') ->
(match compute_displayed_name_in RenamingForGoal avoid name c' with
- | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+ | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| Cast (c,_,_) -> lookup avoid n c
| _ -> None
@@ -191,9 +191,9 @@ let lookup_index_as_renamed env t n =
(match compute_displayed_name_in RenamingForGoal [] name c' with
(Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
- if n=0 then
+ if Int.equal n 0 then
Some (d-1)
- else if n=1 then
+ else if Int.equal n 1 then
Some d
else
lookup (n-1) (d+1) c')
@@ -201,15 +201,15 @@ let lookup_index_as_renamed env t n =
(match compute_displayed_name_in RenamingForGoal [] name c' with
| (Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
- if n=0 then
+ if Int.equal n 0 then
Some (d-1)
- else if n=1 then
+ else if Int.equal n 1 then
Some d
else
lookup (n-1) (d+1) c'
)
| Cast (c,_,_) -> lookup n d c
- | _ -> if n=0 then Some (d-1) else None
+ | _ -> if Int.equal n 0 then Some (d-1) else None
in lookup n 1 t
(**********************************************************************)
@@ -224,7 +224,7 @@ let update_name na ((_,e),c) =
let rec decomp_branch n nal b (avoid,env as e) c =
let flag = if b then RenamingForGoal else RenamingForCasesPattern in
- if n=0 then (List.rev nal,(e,c))
+ if Int.equal n 0 then (List.rev nal,(e,c))
else
let na,c,f =
match kind_of_term (strip_outer_cast c) with
@@ -247,7 +247,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
| [] -> [[],rhs]
| na::nal ->
match kind_of_term c with
- | Case (ci,p,c,cl) when c = mkRel (List.index na (snd e))
+ | Case (ci,p,c,cl) when eq_constr c (mkRel (List.index na (snd e)))
& (* don't contract if p dependent *)
computable p (ci.ci_pp_info.ind_nargs) ->
let clauses = build_tree na isgoal e ci cl in
@@ -278,7 +278,7 @@ let is_nondep_branch c n =
false
let extract_nondep_branches test c b n =
- let rec strip n r = if n=0 then r else
+ let rec strip n r = if Int.equal n 0 then r else
match r with
| GLambda (_,_,_,_,t) -> strip (n-1) t
| GLetIn (_,_,_,t) -> strip (n-1) t
@@ -287,7 +287,7 @@ let extract_nondep_branches test c b n =
let it_destRLambda_or_LetIn_names n c =
let rec aux n nal c =
- if n=0 then (List.rev nal,c) else match c with
+ if Int.equal n 0 then (List.rev nal,c) else match c with
| GLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
| GLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
| _ ->
@@ -311,7 +311,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
let synth_type = synthetize_type () in
let tomatch = detype c in
let alias, aliastyp, pred=
- if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0
+ if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0)
then
Anonymous, None, None
else
@@ -323,7 +323,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
| GLambda (_,x,_,t,c) -> x, c
| _ -> Anonymous, typ in
let aliastyp =
- if List.for_all ((=) Anonymous) nl then None
+ if List.for_all (name_eq Anonymous) nl then None
else Some (dl,indsp,nl) in
n, aliastyp, Some typ
in
@@ -332,7 +332,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
try
if !Flags.raw_print then
RegularStyle
- else if st = LetPatternStyle then
+ else if st == LetPatternStyle then
st
else if PrintingLet.active indsp then
LetStyle
@@ -342,16 +342,16 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
st
with Not_found -> st
in
- match tag with
- | LetStyle when aliastyp = None ->
+ match tag, aliastyp with
+ | LetStyle, None ->
let bl' = Array.map detype bl in
let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
GLetTuple (dl,nal,(alias,pred),tomatch,d)
- | IfStyle when aliastyp = None ->
+ | IfStyle, None ->
let bl' = Array.map detype bl in
let nondepbrs =
Array.map3 (extract_nondep_branches testdep) bl bl' consnargsl in
- if Array.for_all ((<>) None) nondepbrs then
+ if Array.for_all ((!=) None) nondepbrs then
GIf (dl,tomatch,(alias,pred),
Option.get nondepbrs.(0),Option.get nondepbrs.(1))
else
@@ -399,7 +399,7 @@ let rec detype (isgoal:bool) avoid env t =
| Cast (c1,k,c2) ->
let d1 = detype isgoal avoid env c1 in
let d2 = detype isgoal avoid env c2 in
- GCast(dl,d1,if k = VMcast then CastVM d2 else CastConv d2)
+ GCast(dl,d1,if k == VMcast then CastVM d2 else CastConv d2)
| Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
| Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
| LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
@@ -512,7 +512,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
in
let rec buildrec ids patlist avoid env n b =
- if n=0 then
+ if Int.equal n 0 then
(dl, ids,
[PatCstr(dl, constr, List.rev patlist,Anonymous)],
detype isgoal avoid env b)
@@ -542,9 +542,9 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
and detype_binder isgoal bk avoid env na ty c =
let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
- let na',avoid' =
- if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
- else compute_displayed_name_in flag avoid na c in
+ let na',avoid' = match bk with
+ | BLetIn -> compute_displayed_let_name_in flag avoid na c
+ | _ -> compute_displayed_name_in flag avoid na c in
let r = detype isgoal avoid' (add_name na' env) c in
match bk with
| BProd -> GProd (dl, na',Explicit,detype false avoid env ty, r)
@@ -560,7 +560,7 @@ let detype_rel_context where avoid env sign =
match where with
| None -> na,avoid
| Some c ->
- if b<>None then
+ if b != None then
compute_displayed_let_name_in
(RenamingElsewhereFor (env,c)) avoid na c
else
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 26b3267133..42dd7201d9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -170,7 +170,7 @@ let ise_array2 evd f v1 v2 =
if b then allrec i' (n-1) else (evd,false)
in
let lv1 = Array.length v1 in
- if lv1 = Array.length v2 then allrec evd (pred lv1)
+ if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
else (evd,false)
let ise_stack2 no_app env evd f sk1 sk2 =
@@ -185,8 +185,8 @@ let ise_stack2 no_app env evd f sk1 sk2 =
let (i'',b'') = ise_array2 i' (fun ii -> f env ii CONV) c1 c2 in
if b'' then ise_stack2 true i'' q1 q2 else fal ()
else fal ()
- | Zfix ((li1,(_,tys1,bds1 as recdef1)),a1)::q1, Zfix ((li2,(_,tys2,bds2)),a2)::q2 ->
- if li1=li2 then
+ | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
+ if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
let (i',b') = ise_and i [
(fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
(fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
@@ -271,6 +271,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
in
ise_try evd [f1; f2; f3] in
+ let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
(* Evar must be undefined since we have flushed evars *)
match (flex_kind_of_term term1 sk1, flex_kind_of_term term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -284,7 +285,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
(position_problem true pbty,ev1,zip(term2,r))
|_, (_, _) -> (i, false)
and f2 i =
- if sp1 = sp2 then
+ if Int.equal sp1 sp2 then
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
|None, (i', true) -> solve_refl (evar_conv_x ts) env i' sp1 al1 al2, true
|_ -> i, false
@@ -336,7 +337,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| (CoFix _|Meta _|Rel _)-> true
| Evar _ -> List.exists (function (Zfix _ | Zcase _) -> true | _ -> false) args
(* false (* immediate solution without Canon Struct *)*)
- | Lambda _ -> assert(args = []); true
+ | Lambda _ -> assert (match args with [] -> true | _ -> false); true
| LetIn (_,b,_,c) ->
is_unnamed (whd_betaiota_deltazeta_for_iota_state ts env i (subst1 b c, args))
| Case _| Fix _| App _| Cast _ -> assert false in
@@ -372,7 +373,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| Rigid, Rigid when isLambda term1 & isLambda term2 ->
let (na,c1,c'1) = destLambda term1 in
let (_,c2,c'2) = destLambda term2 in
- assert (sk1=[] & sk2=[]);
+ assert app_empty;
ise_and evd
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
@@ -419,7 +420,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
(* Eta-expansion *)
| Rigid, _ when isLambda term1 ->
- assert (sk1 = []);
+ assert (match sk1 with [] -> true | _ -> false);
let (na,c1,c'1) = destLambda term1 in
let c = nf_evar evd c1 in
let env' = push_rel (na,None,c) env in
@@ -428,7 +429,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
evar_eqappr_x ts env' evd CONV appr1 appr2
| _, Rigid when isLambda term2 ->
- assert (sk2 = []);
+ assert (match sk2 with [] -> true | _ -> false);
let (na,c2,c'2) = destLambda term2 in
let c = nf_evar evd c2 in
let env' = push_rel (na,None,c) env in
@@ -439,17 +440,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| Rigid, Rigid -> begin
match kind_of_term term1, kind_of_term term2 with
- | Sort s1, Sort s2 when sk1=[] & sk2=[] ->
+ | Sort s1, Sort s2 when app_empty ->
(try
let evd' =
- if pbty = CONV
+ if pbty == CONV
then Evd.set_eq_sort evd s1 s2
else Evd.set_leq_sort evd s1 s2
in (evd', true)
with Univ.UniverseInconsistency _ -> (evd, false)
| _ -> (evd, false))
- | Prod (n,c1,c'1), Prod (_,c2,c'2) when sk1=[] & sk2=[] ->
+ | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
ise_and evd
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
@@ -467,7 +468,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
else (evd, false)
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
- if i1=i2 then
+ if Int.equal i1 i2 then
ise_and evd
[(fun i -> ise_array2 i
(fun i -> evar_conv_x ts env i CONV) tys1 tys2);
@@ -489,8 +490,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| PseudoRigid, PseudoRigid ->
begin match kind_of_term term1, kind_of_term term2 with
- | Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) -> (* Partially applied fixs *)
- if li1=li2 then
+ | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
+ if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
ise_and evd [
(fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2);
(fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2);
@@ -512,7 +513,7 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
let (evd',ks,_) =
List.fold_left
(fun (i,ks,m) b ->
- if m=n then (i,t2::ks, m-1) else
+ if Int.equal m n then (i,t2::ks, m-1) else
let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
let (i',ev) = new_evar i env ~src:dloc (substl ks b) in
(i', ev :: ks, m - 1))
@@ -553,8 +554,9 @@ let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
let subst = make_pure_subst evi args in
let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in
- if subst' = [] then evd, false else
- Evd.define evk (mkVar (fst (List.hd subst'))) evd, true
+ match subst' with
+ | [] -> evd, false
+ | (id, _) :: _ -> Evd.define evk (mkVar id) evd, true
let apply_on_subterm f c t =
let rec applyrec (k,c as kc) t =
@@ -614,10 +616,12 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let rec make_subst = function
| (id,_,t)::ctxt', c::l, occs::occsl when isVarId id c ->
- if occs<>None then
+ begin match occs with
+ | Some _ ->
error "Cannot force abstraction on identity instance."
- else
+ | None ->
make_subst (ctxt',l,occsl)
+ end
| (id,_,t)::ctxt', c::l, occs::occsl ->
let evs = ref [] in
let ty = Retyping.get_type_of env_rhs evd c in
@@ -698,18 +702,19 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = decompose_app t1 in
let (term2,l2 as appr2) = decompose_app t2 in
+ let app_empty = match l1, l2 with [], [] -> true | _ -> false in
match kind_of_term term1, kind_of_term term2 with
- | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
- & Array.for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
+ | Evar (evk1,args1), (Rel _|Var _) when app_empty
+ && Array.for_all (fun a -> eq_constr a term2 || isEvar a) args1 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
choose_less_dependent_instance evk1 evd term2 args1
- | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
- & Array.for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
+ | (Rel _|Var _), Evar (evk2,args2) when app_empty
+ && Array.for_all (fun a -> eq_constr a term1 || isEvar a) args2 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
choose_less_dependent_instance evk2 evd term1 args2
- | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 ->
+ | Evar (evk1,args1), Evar (evk2,args2) when Int.equal evk1 evk2 ->
let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in
solve_refl ~can_drop:true f env evd evk1 args1 args2, true
| Evar ev1, Evar ev2 ->
@@ -796,9 +801,11 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
if b then
let (evd', rest) = extract_all_conv_pbs evd' in
- if rest = [] then aux evd' pbs true stuck
- else (* Unification got actually stuck, postpone *)
+ begin match rest with
+ | [] -> aux evd' pbs true stuck
+ | _ -> (* Unification got actually stuck, postpone *)
aux evd pbs progress (pb :: stuck)
+ end
else Pretype_errors.error_cannot_unify env evd (t1, t2)
| _ ->
if progress then aux evd stuck false []
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7ccc9d493e..37f698cbe7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -146,7 +146,7 @@ let noccur_evar evd evk c =
| Evar (evk',_ as ev') ->
(match safe_evar_value evd ev' with
| Some c -> occur_rec c
- | None -> if evk = evk' then raise Occur)
+ | None -> if Int.equal evk evk' then raise Occur)
| _ -> iter_constr occur_rec c
in
try occur_rec c; true with Occur -> false
@@ -357,28 +357,36 @@ let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?ca
* Restricting existing evars *
*------------------------------------*)
+let rec eq_filter l1 l2 = match l1, l2 with
+| [], [] -> true
+| h1 :: l1, h2 :: l2 ->
+ (if h1 then h2 else not h2) && eq_filter l1 l2
+| _ -> false
+
let restrict_evar_key evd evk filter candidates =
- if filter = None && candidates = None then
- evd,evk
- else
+ match filter, candidates with
+ | None, None -> evd, evk
+ | _ ->
let evi = Evd.find_undefined evd evk in
let oldfilter = evar_filter evi in
- if filter = Some oldfilter && candidates = None then
- evd,evk
- else
- let filter =
- match filter with
+ begin match filter, candidates with
+ | Some filter, None when eq_filter oldfilter filter ->
+ evd, evk
+ | _ ->
+ let filter = match filter with
| None -> evar_filter evi
| Some filter -> filter in
- let candidates =
- match candidates with None -> evi.evar_candidates | _ -> candidates in
- let ccl = evi.evar_concl in
- let sign = evar_hyps evi in
- let src = evi.evar_source in
- let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
- let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
- let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
- Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
+ let candidates = match candidates with
+ | None -> evi.evar_candidates
+ | Some _ -> candidates in
+ let ccl = evi.evar_concl in
+ let sign = evar_hyps evi in
+ let src = evi.evar_source in
+ let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
+ let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
+ let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
+ Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
+ end
(* Restrict an applied evar and returns its restriction in the same context *)
let restrict_applied_evar evd (evk,argsv) filter candidates =
@@ -459,7 +467,7 @@ let make_alias_map env =
(var_aliases,rel_aliases)
let lift_aliases n (var_aliases,rel_aliases as aliases) =
- if n = 0 then aliases else
+ if Int.equal n 0 then aliases else
(var_aliases,
Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l))
rel_aliases Intmap.empty)
@@ -631,7 +639,9 @@ let rec check_and_clear_in_constr evdref err ids c =
with ClearDependencyError (rid,err) ->
raise (ClearDependencyError (List.assoc rid rids,err)) in
- if rids = [] then c else begin
+ begin match rids with
+ | [] -> c
+ | _ ->
let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
evdref := Evd.define evk ev' !evdref;
@@ -757,7 +767,10 @@ let is_unification_pattern_evar env evd (evk,args) l t =
None
let is_unification_pattern_pure_evar env evd (evk,args) t =
- is_unification_pattern_evar env evd (evk,args) [] t <> None
+ let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
+ match is_ev with
+ | None -> false
+ | Some _ -> true
let is_unification_pattern (env,nb) evd f l t =
match kind_of_term f with
@@ -984,8 +997,9 @@ let rec assoc_up_to_alias sigma aliases y yc = function
let c' = whd_evar sigma c in
if eq_constr y c' then id
else
- if l <> [] then assoc_up_to_alias sigma aliases y yc l
- else
+ match l with
+ | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
+ | [] ->
(* Last chance, we reason up to alias conversion *)
match (if c == c' then cc else normalize_alias_opt aliases c') with
| Some cc when eq_constr yc cc -> id
@@ -1184,7 +1198,7 @@ let closure_of_filter evd evk filter =
let ids = List.map pi1 (evar_context evi) in
let test id b = b || Idset.mem id vars in
let newfilter = List.map2 test ids filter in
- if newfilter = evar_filter evi then None else Some newfilter
+ if eq_filter newfilter (evar_filter evi) then None else Some newfilter
let restrict_hyps evd evk filter candidates =
(* What to do with dependencies?
@@ -1236,13 +1250,14 @@ let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
| None -> None
| Some filter -> closure_of_filter evd evk filter in
let candidates = extract_candidates sols in
- if candidates <> None then
- restrict_evar evd evk filter candidates
- else
+ match candidates with
+ | None ->
(* We made an approximation by not expanding a local definition *)
let evd,ev = restrict_applied_evar evd ev filter None in
let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
Evd.add_conv_pb pb evd
+ | Some _ ->
+ restrict_evar evd evk filter candidates
(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
@@ -1287,11 +1302,11 @@ let are_canonical_instances args1 args2 env =
aux (n+1) sign
| [] ->
let rec aux2 n =
- n = n1 ||
+ Int.equal n n1 ||
(isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
in aux2 n
| _ -> false in
- n1 = n2 & aux 0 (named_context env)
+ Int.equal n1 n2 && aux 0 (named_context env)
let filter_compatible_candidates conv_algo env evd evi args rhs c =
let c' = instantiate_evar (evar_filtered_context evi) c args in
@@ -1313,10 +1328,15 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
let args2 = Array.to_list argsv2 in
let l1' = List.filter (fun c1 ->
let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
- List.filter (fun c2 ->
- (filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2
- <> None)) l2 <> []) l1 in
- if List.length l1 = List.length l1' then None else Some l1'
+ let filter c2 =
+ let compatibility = filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 in
+ match compatibility with
+ | None -> false
+ | Some _ -> true
+ in
+ let filtered = List.filter filter l2 in
+ match filtered with [] -> false | _ -> true) l1 in
+ if Int.equal (List.length l1) (List.length l1') then None else Some l1'
exception CannotProject of bool list option
@@ -1342,7 +1362,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
Array.for_all (is_constrainable_in k g) params
| Ind _ -> Array.for_all (is_constrainable_in k g) args
| Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
- | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
+ | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
| Var id -> Idset.mem id fv_ids
| Rel n -> n <= k || Intset.mem n fv_rels
| Sort _ -> true
@@ -1449,7 +1469,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
| None -> None
| Some filter -> closure_of_filter evd evk filter in
let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
- if fst ev1 = evk & can_drop then (* No refinement *) evd else
+ if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
(* either progress, or not allowed to drop, e.g. to preserve possibly *)
(* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
(* if e can depend on x until ?y is not resolved, or, conversely, we *)
@@ -1549,11 +1569,13 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
let filter = closure_of_filter evd evk' filter in
let candidates = extract_candidates sols in
- let evd =
- if candidates <> None then restrict_evar evd evk' filter candidates
- else
- let evd,ev'' = restrict_applied_evar evd ev' filter None in
- Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd in
+ let evd = match candidates with
+ | None ->
+ let evd, ev'' = restrict_applied_evar evd ev' filter None in
+ Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd
+ | Some _ ->
+ restrict_evar evd evk' filter candidates
+ in
evdref := evd;
evar in
@@ -1573,7 +1595,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
try project_variable t
with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
| Evar (evk',args' as ev') ->
- if evk = evk' then raise (OccurCheckIn (evd,rhs));
+ if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs));
(* Evar/Evar problem (but left evar is virtual) *)
let aliases = lift_aliases k aliases in
(try
@@ -1653,7 +1675,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
match kind_of_term rhs with
| Evar (evk2,argsv2 as ev2) ->
- if evk = evk2 then
+ if Int.equal evk evk2 then
solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
else
solve_evar_evar ~force:choose
@@ -1696,7 +1718,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
(* last chance: rhs actually reduces to ev *)
let c = whd_betadeltaiota env evd rhs in
match kind_of_term c with
- | Evar (evk',argsv2) when evk = evk' ->
+ | Evar (evk',argsv2) when Int.equal evk evk' ->
solve_refl
(fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
env evd evk argsv argsv2
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d24509c858..98f8230a6f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -61,11 +61,17 @@ let evar_env evi =
List.fold_right push_named (evar_filtered_context evi)
(reset_context (Global.env()))
+let eq_evar_body b1 b2 = match b1, b2 with
+| Evar_empty, Evar_empty -> true
+| Evar_defined t1, Evar_defined t2 -> eq_constr t1 t2
+| _ -> false
+
let eq_evar_info ei1 ei2 =
ei1 == ei2 ||
eq_constr ei1.evar_concl ei2.evar_concl &&
eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) &&
- ei1.evar_body = ei2.evar_body
+ eq_evar_body ei1.evar_body ei2.evar_body
+ (** ppedrot: [eq_constr] may be a bit too permissive here *)
(* spiwack: Revised hierarchy :
- ExistentialMap ( Maps of existential_keys )
@@ -92,7 +98,9 @@ let make_evar_instance sign args =
let instantiate_evar sign c args =
let inst = make_evar_instance sign args in
- if inst = [] then c else replace_vars inst c
+ match inst with
+ | [] -> c
+ | _ -> replace_vars inst c
module EvarInfoMap = struct
type t = evar_info ExistentialMap.t * evar_info ExistentialMap.t
@@ -216,9 +224,10 @@ module EvarMap = struct
let existential_value (sigma,_) = EvarInfoMap.existential_value sigma
let existential_type (sigma,_) = EvarInfoMap.existential_type sigma
let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma
- let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) &&
+ let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) =
+ not (x == y) &&
(EvarInfoMap.exists_undefined sigma1
- (fun k v -> assert (v.evar_body = Evar_empty);
+ (fun k v -> assert (v.evar_body == Evar_empty);
EvarInfoMap.is_defined sigma2 k))
let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
@@ -260,6 +269,8 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
type instance_constraint = IsSuperType | IsSubType | Conv
+let eq_instance_constraint c1 c2 = c1 == c2
+
(* Status of the unification of the type of an instance against the type of
the meta it instantiates:
- CoerceToType means that the unification of types has not been done
@@ -361,7 +372,7 @@ let add_constraints d e = {d with evars= EvarMap.add_constraints d.evars e}
(* evar_map are considered empty disregarding histories *)
let is_empty d =
EvarMap.is_empty d.evars &&
- d.conv_pbs = [] &&
+ begin match d.conv_pbs with [] -> true | _ -> false end &&
Metamap.is_empty d.metas
let subst_named_context_val s = map_named_val (subst_mps s)
@@ -376,7 +387,7 @@ let subst_evar_info s evi =
let subst_evar_defs_light sub evd =
assert (Univ.is_initial_universes (snd (snd evd.evars)));
- assert (evd.conv_pbs = []);
+ assert (match evd.conv_pbs with [] -> true | _ -> false);
{ evd with
metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
evars = EvarInfoMap.map (subst_evar_info sub) (fst evd.evars), (snd evd.evars)
@@ -417,13 +428,12 @@ let define evk body evd =
| _ -> ExistentialSet.add evk evd.last_mods }
let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates evd =
- let filter =
- if filter = None then
- List.map (fun _ -> true) (named_context_of_val hyps)
- else
- (let filter = Option.get filter in
- assert (List.length filter = List.length (named_context_of_val hyps));
- filter)
+ let filter = match filter with
+ | None ->
+ List.map (fun _ -> true) (named_context_of_val hyps)
+ | Some filter ->
+ assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)));
+ filter
in
{ evd with
evars = EvarMap.add_undefined evd.evars evk
@@ -504,31 +514,34 @@ let univ_of_sort = function
| Prop Null -> Univ.type0m_univ
let is_eq_sort s1 s2 =
- if s1 = s2 then None
- else
- let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in
- if u1 = u2 then None
+ if Pervasives.(=) s1 s2 then None (* FIXME *)
+ else
+ let u1 = univ_of_sort s1
+ and u2 = univ_of_sort s2 in
+ if Pervasives.(=) u1 u2 then None (* FIXME *)
else Some (u1, u2)
-let is_univ_var_or_set u =
- Univ.is_univ_variable u || u = Univ.type0_univ
+let is_univ_var_or_set u =
+ Univ.is_univ_variable u || Pervasives.(=) u Univ.type0_univ (** FIXME *)
let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
match is_eq_sort s1 s2 with
| None -> d
| Some (u1, u2) ->
- match s1, s2 with
- | Prop c, Prop c' ->
- if c = Null && c' = Pos then d
- else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[])))
- | Type u, Prop c ->
- if c = Pos then
- add_constraints d (Univ.enforce_leq u Univ.type0_univ Univ.empty_constraint)
- else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
- | _, Type u ->
- if is_univ_var_or_set u then
- add_constraints d (Univ.enforce_leq u1 u2 Univ.empty_constraint)
- else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
+ match s1, s2 with
+ | Prop Null, Prop Pos -> d
+ | Prop _, Prop _ ->
+ raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
+ | Type u, Prop Pos ->
+ let cstr = Univ.enforce_leq u Univ.type0_univ Univ.empty_constraint in
+ add_constraints d cstr
+ | Type _, Prop _ ->
+ raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
+ | _, Type u ->
+ if is_univ_var_or_set u then
+ let cstr = Univ.enforce_leq u1 u2 Univ.empty_constraint in
+ add_constraints d cstr
+ else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2,[]))
let is_univ_level_var us u =
match Univ.universe_level u with
@@ -637,7 +650,7 @@ let meta_with_name evd id =
Metamap.fold
(fun n clb (l1,l2 as l) ->
let (na',def) = clb_name clb in
- if na = na' then if def then (n::l1,l2) else (n::l1,n::l2)
+ if name_eq na na' then if def then (n::l1,l2) else (n::l1,n::l2)
else l)
evd.metas ([],[]) in
match mvnodef, mvl with
@@ -790,7 +803,7 @@ let evar_dependency_closure n sigma =
let graph = compute_evar_dependency_graph sigma in
let order a b = fst a < fst b in
let rec aux n l =
- if n=0 then l
+ if Int.equal n 0 then l
else
let l' =
List.map_append (fun (evk,_) ->
@@ -815,7 +828,7 @@ let pr_evar_map_t depth sigma =
| Some n ->
(* Print all evars *)
str"UNDEFINED EVARS"++
- (if n=0 then mt() else str" (+level "++int n++str" closure):")++
+ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
brk(0,1)++
pr_evar_list (evar_dependency_closure n sigma)++fnl()
and svs =
@@ -850,15 +863,19 @@ let pr_constraints pbs =
spc() ++ print_constr t2) pbs)
let pr_evar_map_constraints evd =
- if evd.conv_pbs = [] then mt()
- else pr_constraints evd.conv_pbs++fnl()
+ match evd.conv_pbs with
+ | [] -> mt ()
+ | _ -> pr_constraints evd.conv_pbs ++ fnl ()
let pr_evar_map allevars evd =
let pp_evm =
if EvarMap.is_empty evd.evars then mt() else
pr_evar_map_t allevars evd++fnl() in
- let cstrs = if evd.conv_pbs = [] then mt() else
- str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
+ let cstrs = match evd.conv_pbs with
+ | [] -> mt ()
+ | _ ->
+ str "CONSTRAINTS:" ++ brk(0,1) ++ pr_constraints evd.conv_pbs ++ fnl ()
+ in
let pp_met =
if Metamap.is_empty evd.metas then mt() else
str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 709303bf5c..a4e314873a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -42,6 +42,9 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
type instance_constraint = IsSuperType | IsSubType | Conv
+val eq_instance_constraint :
+ instance_constraint -> instance_constraint -> bool
+
(** Status of the unification of the type of an instance against the type of
the meta it instantiates:
- CoerceToType means that the unification of types has not been done
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 09225b2f65..7ef0bd1f70 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -108,13 +108,20 @@ let fold_glob_constr f acc =
let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
+let same_id na id = match na with
+| Anonymous -> false
+| Name id' -> id_eq id id'
+
let occur_glob_constr id =
let rec occur = function
- | GVar (loc,id') -> id = id'
+ | GVar (loc,id') -> id_eq id id'
| GApp (loc,f,args) -> (occur f) or (List.exists occur args)
- | GLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
- | GProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
- | GLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
+ | GLambda (loc,na,bk,ty,c) ->
+ (occur ty) || (not (same_id na id) && (occur c))
+ | GProd (loc,na,bk,ty,c) ->
+ (occur ty) || (not (same_id na id) && (occur c))
+ | GLetIn (loc,na,b,c) ->
+ (occur b) || (not (same_id na id) && (occur c))
| GCases (loc,sty,rtntypopt,tml,pl) ->
(occur_option rtntypopt)
or (List.exists (fun (tm,_) -> occur tm) tml)
@@ -127,13 +134,13 @@ let occur_glob_constr id =
| GRec (loc,fk,idl,bl,tyl,bv) ->
not (Array.for_all4 (fun fid bl ty bd ->
let rec occur_fix = function
- [] -> not (occur ty) && (fid=id or not(occur bd))
+ [] -> not (occur ty) && (id_eq fid id || not(occur bd))
| (na,k,bbd,bty)::bl ->
not (occur bty) &&
(match bbd with
Some bd -> not (occur bd)
| _ -> true) &&
- (na=Name id or not(occur_fix bl)) in
+ (match na with Name id' -> id_eq id id' | _ -> not (occur_fix bl)) in
occur_fix bl)
idl bl tyl bv)
| GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false)
@@ -143,7 +150,7 @@ let occur_glob_constr id =
and occur_option = function None -> false | Some p -> occur p
- and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
+ and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt
in occur
@@ -233,10 +240,13 @@ let loc_of_glob_constr = function
(* Conversion from glob_constr to cases pattern, if possible *)
let rec cases_pattern_of_glob_constr na = function
- | GVar (loc,id) when na<>Anonymous ->
+ | GVar (loc,id) ->
+ begin match na with
+ | Name _ ->
(* Unable to manage the presence of both an alias and a variable *)
raise Not_found
- | GVar (loc,id) -> PatVar (loc,Name id)
+ | Anonymous -> PatVar (loc,Name id)
+ end
| GHole (loc,_) -> PatVar (loc,na)
| GRef (loc,ConstructRef cstr) ->
PatCstr (loc,cstr,[],na)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 15255ea270..257ad448ad 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -67,7 +67,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
let constrs = get_constructors env indf in
let rec add_branch env k =
- if k = Array.length mip.mind_consnames then
+ if Int.equal k (Array.length mip.mind_consnames) then
let nbprod = k+1 in
let indf' = lift_inductive_family nbprod indf in
@@ -284,7 +284,7 @@ let mis_make_indrec env sigma listdepkind mib =
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
(* recarg information for non recursive parameters *)
let rec recargparn l n =
- if n = 0 then l else recargparn (mk_norec::l) (n-1) in
+ if Int.equal n 0 then l else recargparn (mk_norec::l) (n-1) in
let recargpar = recargparn [] (nparams-nparrec) in
let make_one_rec p =
let makefix nbconstruct =
@@ -390,7 +390,7 @@ let mis_make_indrec env sigma listdepkind mib =
let tyi = snd indi in
let nconstr = Array.length mipi.mind_consnames in
let rec onerec env j =
- if j = nconstr then
+ if Int.equal j nconstr then
make_branch env (i+j) rest
else
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
@@ -442,7 +442,10 @@ let build_case_analysis_scheme env sigma ity dep kind =
let build_case_analysis_scheme_default env sigma ity kind =
let (mib,mip) = lookup_mind_specif env ity in
- let dep = inductive_sort_family mip <> InProp in
+ let dep = match inductive_sort_family mip with
+ | InProp -> false
+ | _ -> true
+ in
mis_make_case_com dep env sigma ity (mib,mip) kind
@@ -465,7 +468,7 @@ let modify_sort_scheme sort =
let rec drec npar elim =
match kind_of_term elim with
| Lambda (n,t,c) ->
- if npar = 0 then
+ if Int.equal npar 0 then
mkLambda (n, change_sort_arity sort t, c)
else
mkLambda (n, t, drec (npar-1) c)
@@ -480,7 +483,7 @@ let weaken_sort_scheme sort npars term =
let rec drec np elim =
match kind_of_term elim with
| Prod (n,t,c) ->
- if np = 0 then
+ if Int.equal np 0 then
let t' = change_sort_arity sort t in
mkProd (n, t', c),
mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
@@ -502,7 +505,7 @@ let check_arities listdepkind =
let _ = List.fold_left
(fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
let kelim = elim_sorts (mibi,mipi) in
- if not (List.exists ((=) kind) kelim) then raise
+ if not (List.exists ((==) kind) kelim) then raise
(RecursionSchemeError
(NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
else if List.mem ni ln then raise
@@ -520,7 +523,7 @@ let build_mutual_induction_scheme env sigma = function
(List.map
(function (mind',dep',s') ->
let (sp',_) = mind' in
- if sp=sp' then
+ if eq_mind sp sp' then
let (mibi',mipi') = lookup_mind_specif env mind' in
(mind',mibi',mipi',dep',s')
else
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index de6873ba3d..d2aaea9fa3 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -146,13 +146,15 @@ let nconstructors ind =
let mis_constructor_has_local_defs (indsp,j) =
let (mib,mip) = Global.lookup_inductive indsp in
- mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
- <> recarg_length mip.mind_recargs j + mib.mind_nparams
+ let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
+ let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
+ not (Int.equal l1 l2)
let inductive_has_local_defs ind =
let (mib,mip) = Global.lookup_inductive ind in
- rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealargs_ctxt
- <> mib.mind_nparams + mip.mind_nrealargs
+ let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealargs_ctxt in
+ let l2 = mib.mind_nparams + mip.mind_nrealargs in
+ not (Int.equal l1 l2)
(* Length of arity (w/o local defs) *)
@@ -257,7 +259,7 @@ let get_arity env (ind,params) =
parameters *)
let parsign = mib.mind_params_ctxt in
let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
- if List.length params = rel_context_nhyps parsign - nnonrecparams then
+ if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
snd (List.chop nnonrecparams mib.mind_params_ctxt)
else
parsign in
@@ -378,7 +380,10 @@ let is_predicate_explicitly_dep env pred arsign =
check whether the predicate is actually dependent or not
would indeed be more natural! *)
- na <> Anonymous
+ begin match na with
+ | Anonymous -> false
+ | Name _ -> true
+ end
| _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate"
in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 0f8c011e20..a456d08cce 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -50,7 +50,7 @@ exception PatternMatchingFailure
let constrain n (ids, m as x) (names, terms as subst) =
try
let (ids',m') = List.assoc n terms in
- if ids = ids' && eq_constr m m' then subst
+ if List.equal id_eq ids ids' && eq_constr m m' then subst
else raise PatternMatchingFailure
with
Not_found ->
@@ -97,7 +97,7 @@ let rec list_insert a = function
let extract_bound_vars =
let rec aux k = function
| ([],_) -> []
- | (n :: l, (na1, na2, _) :: stk) when k - n = 0 ->
+ | (n :: l, (na1, na2, _) :: stk) when Int.equal k n ->
begin match na1, na2 with
| Name id1, Name _ -> list_insert id1 (aux (k + 1) (l, stk))
| Name _, Anonymous -> anomaly "Unnamed bound variable"
@@ -122,7 +122,7 @@ let rec make_renaming ids = function
let merge_binding allow_bound_rels stk n cT subst =
let depth = List.length stk in
let c =
- if depth = 0 then
+ if Int.equal depth 0 then
(* Optimization *)
([],cT)
else
@@ -162,13 +162,13 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
| PMeta None, m -> subst
- | PRef (VarRef v1), Var v2 when id_ord v1 v2 = 0 -> subst
+ | PRef (VarRef v1), Var v2 when id_eq v1 v2 -> subst
- | PVar v1, Var v2 when id_ord v1 v2 = 0 -> subst
+ | PVar v1, Var v2 when id_eq v1 v2 -> subst
| PRef ref, _ when conv (constr_of_global ref) cT -> subst
- | PRel n1, Rel n2 when n1 - n2 = 0 -> subst
+ | PRel n1, Rel n2 when Int.equal n1 n2 -> subst
| PSort GProp, Sort (Prop Null) -> subst
@@ -231,7 +231,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
in
let () =
- if not ci1.cip_extensible && List.length br1 <> n2
+ if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
then raise PatternMatchingFailure
in
let chk_branch subst (j,n,c) =
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 36355e1303..c7f51d17bb 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -30,7 +30,7 @@ let is_imported_modpath mp =
match mp with
| MPfile dp ->
let rec find_prefix = function
- |MPfile dp1 -> not (dp1=dp)
+ |MPfile dp1 -> not (dir_path_eq dp1 dp)
|MPdot(mp,_) -> find_prefix mp
|MPbound(_) -> false
in find_prefix current_mp
@@ -234,14 +234,21 @@ let make_all_name_different env =
subscript *)
let occur_rel p env id =
- try lookup_name_of_rel p env = Name id
+ try
+ let name = lookup_name_of_rel p env in
+ begin match name with
+ | Name id' -> id_eq id' id
+ | Anonymous -> false
+ end
with Not_found -> false (* Unbound indice : may happen in debug *)
let visibly_occur_id id (nenv,c) =
let rec occur n c = match kind_of_term c with
| Const _ | Ind _ | Construct _ | Var _
- when shortest_qualid_of_global Idset.empty (global_of_constr c)
- = qualid_of_ident id -> raise Occur
+ when
+ let short = shortest_qualid_of_global Idset.empty (global_of_constr c) in
+ qualid_eq short (qualid_of_ident id) ->
+ raise Occur
| Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
| _ -> iter_constr_with_binders succ occur n c
in
@@ -294,17 +301,19 @@ let next_name_for_display flags =
(* Remark: Anonymous var may be dependent in Evar's contexts *)
let compute_displayed_name_in flags avoid na c =
- if na = Anonymous & noccurn 1 c then
+ match na with
+ | Anonymous when noccurn 1 c ->
(Anonymous,avoid)
- else
+ | _ ->
let fresh_id = next_name_for_display flags na avoid in
let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
(idopt, fresh_id::avoid)
let compute_and_force_displayed_name_in flags avoid na c =
- if na = Anonymous & noccurn 1 c then
+ match na with
+ | Anonymous when noccurn 1 c ->
(Anonymous,avoid)
- else
+ | _ ->
let fresh_id = next_name_for_display flags na avoid in
(Name fresh_id, fresh_id::avoid)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 1f16385a62..bd08df5334 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -134,7 +134,10 @@ let map_pattern_with_binders g f l = function
| PFix _ | PCoFix _ as x) -> x
let error_instantiate_pattern id l =
- let is = if List.length l = 1 then "is" else "are" in
+ let is = match l with
+ | [_] -> "is"
+ | _ -> "are"
+ in
errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
@@ -326,8 +329,11 @@ and pats_of_glob_branches loc metas vars ind brs =
| [] -> false, []
| [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
| (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs ->
- if ind <> None && ind <> Some indsp then
- err loc (Pp.str "All constructors must be in the same inductive type.");
+ let () = match ind with
+ | Some sp when eq_ind sp indsp -> ()
+ | _ ->
+ err loc (Pp.str "All constructors must be in the same inductive type.")
+ in
if Intset.mem (j-1) indexes then
err loc
(str "No unique branch for " ++ int j ++ str"-th constructor.");
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8c216d99b3..674c7e19ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -64,11 +64,12 @@ exception Found of int array
let search_guard loc env possible_indexes fixdefs =
(* Standard situation with only one possibility for each fix. *)
(* We treat it separately in order to get proper error msg. *)
- if List.for_all (fun l->1=List.length l) possible_indexes then
+ let is_singleton = function [_] -> true | _ -> false in
+ if List.for_all is_singleton possible_indexes then
let indexes = Array.of_list (List.map List.hd possible_indexes) in
let fix = ((indexes, 0),fixdefs) in
(try check_fix env fix with
- | e -> if loc = Loc.ghost then raise e else Loc.raise loc e);
+ | e -> Loc.raise loc e);
indexes
else
(* we now search recursively amoungst all combinations *)
@@ -81,7 +82,6 @@ let search_guard loc env possible_indexes fixdefs =
with TypeError _ -> ())
(List.combinations possible_indexes);
let errmsg = "Cannot guess decreasing argument of fix." in
- if loc = Loc.ghost then error errmsg else
user_err_loc (loc,"search_guard", Pp.str errmsg)
with Found indexes -> indexes)
@@ -165,7 +165,7 @@ let evd_comb2 f evdref x y =
let evar_type_fixpoint loc env evdref lna lar vdefj =
let lt = Array.length vdefj in
- if Array.length lar = lt then
+ if Int.equal (Array.length lar) lt then
for i = 0 to lt-1 do
if not (e_cumul env evdref (vdefj.(i)).uj_type
(lift lt lar.(i))) then
@@ -384,14 +384,14 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
| Some ty ->
let (ind, i) = destConstruct fj.uj_val in
let npars = inductive_nparams ind in
- if npars = 0 then []
+ if Int.equal npars 0 then []
else
try
(* Does not treat partially applied constructors. *)
let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in
let IndType (indf, args) = find_rectype env !evdref ty in
let (ind',pars) = dest_ind_family indf in
- if ind = ind' then pars
+ if eq_ind ind ind' then pars
else (* Let the usual code throw an error *) []
with Not_found -> []
else []
@@ -462,14 +462,14 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
| GProd(loc,name,bk,c1,c2) ->
let j = pretype_type empty_valcon env evdref lvar c1 in
- let j' =
- if name = Anonymous then
- let j = pretype_type empty_valcon env evdref lvar c2 in
- { j with utj_val = lift 1 j.utj_val }
- else
- let var = (name,j.utj_val) in
- let env' = push_rel_assum var env in
- pretype_type empty_valcon env' evdref lvar c2
+ let j' = match name with
+ | Anonymous ->
+ let j = pretype_type empty_valcon env evdref lvar c2 in
+ { j with utj_val = lift 1 j.utj_val }
+ | Name _ ->
+ let var = (name,j.utj_val) in
+ let env' = push_rel_assum var env in
+ pretype_type empty_valcon env' evdref lvar c2
in
let resj =
try judge_of_product env name j j'
@@ -500,11 +500,11 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
error_case_not_inductive_loc cloc env !evdref cj
in
let cstrs = get_constructors env indf in
- if Array.length cstrs <> 1 then
+ if not (Int.equal (Array.length cstrs) 1) then
user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
str " with one constructor.");
let cs = cstrs.(0) in
- if List.length nal <> cs.cs_nargs then
+ if not (Int.equal (List.length nal) cs.cs_nargs) then
user_err_loc (loc,"", str "Destructing let on this type expects " ++
int cs.cs_nargs ++ str " variables.");
let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
@@ -568,7 +568,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
let cloc = loc_of_glob_constr c in
error_case_not_inductive_loc cloc env !evdref cj in
let cstrs = get_constructors env indf in
- if Array.length cstrs <> 2 then
+ if not (Int.equal (Array.length cstrs) 2) then
user_err_loc (loc,"",
str "If is only for inductive types with two constructors.");
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fdc7875d73..23de3eb194 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -265,7 +265,7 @@ let pr_cs_pattern = function
| Sort_cs s -> Termops.pr_sort_family s
let open_canonical_structure i (_,o) =
- if i=1 then
+ if Int.equal i 1 then
let lo = compute_canonical_projections o in
List.iter (fun ((proj,cs_pat),s) ->
let l = try Refmap.find proj !object_table with Not_found -> [] in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 405e089a68..256eb6ce81 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -317,8 +317,8 @@ let rec whd_state_gen flags ts env sigma =
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec' (Array.last cl, empty_stack) in
- match kind_of_term x' with
- | Rel 1 when l' = empty_stack ->
+ match kind_of_term x', l' with
+ | Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
let u = if Int.equal napp 1 then f else appvect (f,lc) in
if noccurn 1 u then (pop u,empty_stack) else s
@@ -373,8 +373,8 @@ let local_whd_state_gen flags sigma =
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec (Array.last cl, empty_stack) in
- match kind_of_term x' with
- | Rel 1 when l' = empty_stack ->
+ match kind_of_term x', l' with
+ | Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
let u = if Int.equal napp 1 then f else appvect (f,lc) in
if noccurn 1 u then (pop u,empty_stack) else s
@@ -623,14 +623,15 @@ let fakey = Profile.declare_profile "fhnf_apply";;
let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
*)
-let is_transparent k =
- Conv_oracle.get_strategy k <> Conv_oracle.Opaque
+let is_transparent k = match Conv_oracle.get_strategy k with
+| Conv_oracle.Opaque -> false
+| _ -> true
(* Conversion utility functions *)
type conversion_test = constraints -> constraints
-let pb_is_equal pb = pb = CONV
+let pb_is_equal pb = pb == CONV
let pb_equal = function
| CUMUL -> CONV
@@ -965,8 +966,9 @@ let meta_reducible_instance evd b =
let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
(match
try
- let g,s = List.assoc m metas in
- if isConstruct g or s <> CoerceToType then Some g else None
+ let g, s = List.assoc m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if isConstruct g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkCase (ci,p,g,bl))
@@ -975,14 +977,17 @@ let meta_reducible_instance evd b =
let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
(match
try
- let g,s = List.assoc m metas in
- if isLambda g or s <> CoerceToType then Some g else None
+ let g, s = List.assoc m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if isLambda g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkApp (g,l))
| None -> mkApp (f,Array.map irec l))
| Meta m ->
- (try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u
+ (try let g, s = List.assoc m metas in
+ let is_coerce = match s with CoerceToType -> true | _ -> false in
+ if not is_coerce then irec g else u
with Not_found -> u)
| _ -> map_constr irec u
in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ce4b830cfb..800945f02a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -42,6 +42,10 @@ let type_of_var env id =
with Not_found ->
anomaly ("type_of: variable "^(string_of_id id)^" unbound")
+let is_impredicative_set env = match Environ.engagement env with
+| Some ImpredicativeSet -> true
+| _ -> false
+
let retype ?(polyprop=true) sigma =
let rec type_of env cstr=
match kind_of_term cstr with
@@ -88,8 +92,7 @@ let retype ?(polyprop=true) sigma =
(match (sort_of env t, sort_of (push_rel (name,None,t) env) c2) with
| _, (Prop Null as s) -> s
| Prop _, (Prop Pos as s) -> s
- | Type _, (Prop Pos as s) when
- Environ.engagement env = Some ImpredicativeSet -> s
+ | Type _, (Prop Pos as s) when is_impredicative_set env -> s
| (Type _, _) | (_, Type _) -> new_Type_sort ()
(*
| Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
@@ -111,8 +114,8 @@ let retype ?(polyprop=true) sigma =
| Sort (Type u) -> InType
| Prod (name,t,c2) ->
let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
- if Environ.engagement env <> Some ImpredicativeSet &&
- s2 = InSet & sort_family_of env t = InType then InType else s2
+ if not (is_impredicative_set env) &&
+ s2 == InSet & sort_family_of env t == InType then InType else s2
| App(f,args) when isGlobalRef f ->
let t = type_of_global_reference_knowing_parameters env f args in
family_of_sort (sort_of_atomic_type env sigma t args)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 29d0fa05e7..fc78b0dcad 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -74,6 +74,14 @@ type evaluable_reference =
| EvalRel of int
| EvalEvar of existential
+let evaluable_reference_eq r1 r2 = match r1, r2 with
+| EvalConst c1, EvalConst c2 -> eq_constant c1 c2
+| EvalVar id1, EvalVar id2 -> id_eq id1 id2
+| EvalRel i1, EvalRel i2 -> Int.equal i1 i2
+| EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
+ Int.equal e1 e2 && Array.equal eq_constr ctx1 ctx2
+| _ -> false
+
let mkEvalRef = function
| EvalConst cst -> mkConst cst
| EvalVar id -> mkVar id
@@ -191,7 +199,9 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
List.iteri (fun i t_i ->
if not (List.mem_assoc (i+1) li) then
let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
- if List.intersect fvs reversible_rels <> [] then raise Elimconst)
+ match List.intersect fvs reversible_rels with
+ | [] -> ()
+ | _ -> raise Elimconst)
labs;
let k = lv.(i) in
if k < nargs then
@@ -209,7 +219,10 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
let invert_name labs l na0 env sigma ref = function
| Name id ->
let minfxargs = List.length l in
- if na0 <> Name id then
+ begin match na0 with
+ | Name id' when id_eq id' id ->
+ Some (minfxargs,ref)
+ | _ ->
let refi = match ref with
| EvalRel _ | EvalEvar _ -> None
| EvalVar id' -> Some (EvalVar id)
@@ -224,10 +237,12 @@ let invert_name labs l na0 env sigma ref = function
let labs',ccl = decompose_lam c in
let _, l' = whd_betalet_stack sigma ccl in
let labs' = List.map snd labs' in
- if labs' = labs & l = l' then Some (minfxargs,ref)
+ (** ppedrot: there used to be generic equality on terms here *)
+ if List.equal eq_constr labs' labs &&
+ List.equal eq_constr l l' then Some (minfxargs,ref)
else None
with Not_found (* Undefined ref *) -> None
- else Some (minfxargs,ref)
+ end
| Anonymous -> None (* Actually, should not occur *)
(* [compute_consteval_direct] expand all constant in a whole, but
@@ -238,7 +253,7 @@ let compute_consteval_direct sigma env ref =
let rec srec env n labs c =
let c',l = whd_betadelta_stack env sigma c in
match kind_of_term c' with
- | Lambda (id,t,g) when l=[] ->
+ | Lambda (id,t,g) when List.is_empty l ->
srec (push_rel (id,None,t) env) (n+1) (t::labs) g
| Fix fix ->
(try check_fix_reversibility labs l fix
@@ -255,7 +270,7 @@ let compute_consteval_mutual_fix sigma env ref =
let c',l = whd_betalet_stack sigma c in
let nargs = List.length l in
match kind_of_term c' with
- | Lambda (na,t,g) when l=[] ->
+ | Lambda (na,t,g) when List.is_empty l ->
srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g
| Fix ((lv,i),(names,_,_)) ->
(* Last known constant wrapping Fix is ref = [labs](Fix l) *)
@@ -283,7 +298,7 @@ let compute_consteval_mutual_fix sigma env ref =
let compute_consteval sigma env ref =
match compute_consteval_direct sigma env ref with
- | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 ->
+ | EliminationFix (_,_,(nbfix,_,_)) when not (Int.equal nbfix 1) ->
compute_consteval_mutual_fix sigma env ref
| elim -> elim
@@ -479,7 +494,7 @@ let reduce_mind_case_use_function func env sigma mia =
if isConst func then
let minargs = List.length mia.mcargs in
fun i ->
- if i = bodynum then Some (minargs,func)
+ if Int.equal i bodynum then Some (minargs,func)
else match names.(i) with
| Anonymous -> None
| Name id ->
@@ -596,9 +611,9 @@ let get_simpl_behaviour r =
try
let b = Refmap.find r !behaviour_table in
let flags =
- if b.b_nargs = max_int then [`SimplNeverUnfold]
+ if Int.equal b.b_nargs max_int then [`SimplNeverUnfold]
else if b.b_dont_expose_case then [`SimplDontExposeCase] else [] in
- Some (b.b_recargs, (if b.b_nargs = max_int then -1 else b.b_nargs), flags)
+ Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags)
with Not_found -> None
let get_behaviour = function
@@ -657,14 +672,15 @@ let rec red_elim_const env sigma ref largs =
| Some (_,n) when nargs < n -> raise Redelimination
| Some (x::l,_) when nargs <= List.fold_left max x l -> raise Redelimination
| Some (l,n) ->
+ let is_empty = match l with [] -> true | _ -> false in
List.fold_left (fun stack i ->
let arg = List.nth stack i in
let rarg = whd_construct_stack env sigma arg in
match kind_of_term (fst rarg) with
| Construct _ -> List.assign stack i (applist rarg)
| _ -> raise Redelimination)
- largs l, n >= 0 && l = [] && nargs >= n,
- n >= 0 && l <> [] && nargs >= n in
+ largs l, n >= 0 && is_empty && nargs >= n,
+ n >= 0 && not is_empty && nargs >= n in
try match reference_eval sigma env ref with
| EliminationCases n when nargs >= n ->
let c = reference_value sigma env ref in
@@ -682,7 +698,7 @@ let rec red_elim_const env sigma ref largs =
| EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
let rec descend ref args =
let c = reference_value sigma env ref in
- if ref = refgoal then
+ if evaluable_reference_eq ref refgoal then
(c,args)
else
let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
@@ -962,7 +978,10 @@ let unfoldoccs env sigma (occs,name) c =
if Int.equal nbocc 1 then
error ((string_of_evaluable_ref env name)^" does not occur.");
let rest = List.filter (fun o -> o >= nbocc) locs in
- if rest <> [] then error_invalid_occurrence rest;
+ let () = match rest with
+ | [] -> ()
+ | _ -> error_invalid_occurrence rest
+ in
nf_betaiotazeta sigma uc
in
match occs with
@@ -1102,11 +1121,12 @@ let isIndRef = function IndRef _ -> true | _ -> false
let reduce_to_ref_gen allow_product env sigma ref t =
if isIndRef ref then
let (mind,t) = reduce_to_ind_gen allow_product env sigma t in
- if IndRef mind <> ref then
+ begin match ref with
+ | IndRef mind' when eq_ind mind mind' -> t
+ | _ ->
errorlabstrm "" (str "Cannot recognize a statement based on " ++
Nametab.pr_global_env Idset.empty ref ++ str".")
- else
- t
+ end
else
(* lazily reduces to match the head of [t] with the expected [ref] *)
let rec elimrec env t l =
@@ -1121,7 +1141,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
Nametab.pr_global_env Idset.empty ref ++ str".")
| _ ->
try
- if global_of_constr c = ref
+ if eq_gr (global_of_constr c) ref
then it_mkProd_or_LetIn t l
else raise Not_found
with Not_found ->
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 8372d31daa..862dbb4fa3 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -117,7 +117,7 @@ struct
let fold2 (f:'a -> 'b -> 'c -> 'a) (acc:'a) (c1:'b t) (c2:'c t) : 'a =
let head w = map (fun _ -> ()) w in
- if compare (head c1) (head c2) <> 0
+ if not (Int.equal (compare (head c1) (head c2)) 0)
then invalid_arg "fold2:compare" else
match c1,c2 with
| (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _) -> acc
@@ -136,7 +136,7 @@ struct
let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
let head w = map (fun _ -> ()) w in
- if compare (head c1) (head c2) <> 0
+ if not (Int.equal (compare (head c1) (head c2)) 0)
then invalid_arg "map2_t:compare" else
match c1,c2 with
| (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _) as cc ->
@@ -283,7 +283,7 @@ struct
let rec e_subst_evar i (t:unit->constr) c =
match kind_of_term c with
- | Evar (j,_) when i=j -> t()
+ | Evar (j,_) when Int.equal i j -> t()
| _ -> map_constr (e_subst_evar i t) c
let subst_evar i c = e_subst_evar i (fun _ -> c)
@@ -312,7 +312,7 @@ struct
) (TDnet.find_match dpat dn) []
let fold_pattern_neutral f =
- fold_pattern (fun acc (mset,m,dn) -> if m=neutral_meta then acc else f m dn acc)
+ fold_pattern (fun acc (mset,m,dn) -> if Int.equal m neutral_meta then acc else f m dn acc)
let fold_pattern_nonlin f =
let defined = ref Gmap.empty in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 333d3948dc..b147637f02 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -161,7 +161,7 @@ let new_Type_sort () = Type (new_univ ())
let refresh_universes_gen strict t =
let modified = ref false in
let rec refresh t = match kind_of_term t with
- | Sort (Type u) when strict or u <> Univ.type0m_univ ->
+ | Sort (Type u) when strict || Pervasives.(<>) u Univ.type0m_univ -> (** FIXME *)
modified := true; new_Type ()
| Prod (na,u,v) -> mkProd (na,u,refresh v)
| _ -> t in
@@ -285,7 +285,7 @@ let decompose_app_vect c =
let adjust_app_list_size f1 l1 f2 l2 =
let len1 = List.length l1 and len2 = List.length l2 in
- if len1 = len2 then (f1,l1,f2,l2)
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
else if len1 < len2 then
let extras,restl2 = List.chop (len2-len1) l2 in
(f1, l1, applist (f2,extras), restl2)
@@ -295,7 +295,7 @@ let adjust_app_list_size f1 l1 f2 l2 =
let adjust_app_array_size f1 l1 f2 l2 =
let len1 = Array.length l1 and len2 = Array.length l2 in
- if len1 = len2 then (f1,l1,f2,l2)
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
else if len1 < len2 then
let extras,restl2 = Array.chop (len2-len1) l2 in
(f1, l1, appvect (f2,extras), restl2)
@@ -514,16 +514,9 @@ let occur_meta_or_existential c =
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
-let occur_const s c =
- let rec occur_rec c = match kind_of_term c with
- | Const sp when sp=s -> raise Occur
- | _ -> iter_constr occur_rec c
- in
- try occur_rec c; false with Occur -> true
-
let occur_evar n c =
let rec occur_rec c = match kind_of_term c with
- | Evar (sp,_) when sp=n -> raise Occur
+ | Evar (sp,_) when Int.equal sp n -> raise Occur
| _ -> iter_constr occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -770,18 +763,20 @@ let subst_closed_term_occ_gen_modulo occs test cl occ t =
let check_used_occurrences nbocc (nowhere_except_in,locs) =
let rest = List.filter (fun o -> o >= nbocc) locs in
- if rest <> [] then error_invalid_occurrence rest
+ match rest with
+ | [] -> ()
+ | _ -> error_invalid_occurrence rest
let proceed_with_occurrences f occs x =
- if occs = NoOccurrences then x
- else begin
+ match occs with
+ | NoOccurrences -> x
+ | _ ->
(* TODO FINISH ADAPTING WITH HUGO *)
let plocs = Locusops.convert_occs occs in
assert (List.for_all (fun x -> x >= 0) (snd plocs));
let (nbocc,x) = f 1 x in
check_used_occurrences nbocc plocs;
x
- end
let make_eq_test c = {
match_fun = (fun c' -> if eq_constr c c' then () else raise NotUnifiable);
@@ -851,7 +846,7 @@ let lookup_name_of_rel p names =
let lookup_rel_of_name id names =
let rec lookrec n = function
| Anonymous :: l -> lookrec (n+1) l
- | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
+ | (Name id') :: l -> if id_eq id' id then n else lookrec (n+1) l
| [] -> raise Not_found
in
lookrec 1 names
@@ -889,8 +884,8 @@ let has_polymorphic_type c =
let base_sort_cmp pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *)
- | (Prop c1, Type u) -> pb = Reduction.CUMUL
+ | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *)
+ | (Prop c1, Type u) -> pb == Reduction.CUMUL
| (Type u1, Type u2) -> true
| _ -> false
@@ -917,8 +912,6 @@ let split_app c = match kind_of_term c with
c::(Array.to_list prev), last
| _ -> assert false
-let hdtl l = List.hd l, List.tl l
-
type subst = (rel_context*constr) Intmap.t
exception CannotFilter
@@ -935,9 +928,14 @@ let filtering env cv_pb c1 c2 =
let rec aux env cv_pb c1 c2 =
match kind_of_term c1, kind_of_term c2 with
| App _, App _ ->
- let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
- aux env cv_pb l1 l2; if p1=[] & p2=[] then () else
- aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2))
+ let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+ let () = aux env cv_pb l1 l2 in
+ begin match p1, p2 with
+ | [], [] -> ()
+ | (h1 :: p1), (h2 :: p2) ->
+ aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+ | _ -> assert false
+ end
| Prod (n,t1,c1), Prod (_,t2,c2) ->
aux env cv_pb t1 t2;
aux ((n,None,t1)::env) cv_pb c1 c2
@@ -992,15 +990,6 @@ let rec eta_reduce_head c =
| _ -> c
-(* alpha-eta conversion : ignore print names and casts *)
-let eta_eq_constr =
- let rec aux t1 t2 =
- let t1 = eta_reduce_head (strip_head_cast t1)
- and t2 = eta_reduce_head (strip_head_cast t2) in
- t1=t2 or compare_constr aux t1 t2
- in aux
-
-
(* iterator on rel context *)
let process_rel_context f env =
let sign = named_context_val env in
@@ -1060,13 +1049,13 @@ let adjust_subst_to_rel_context sign l =
let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
let rec mem_named_context id = function
- | (id',_,_) :: _ when id=id' -> true
+ | (id',_,_) :: _ when id_eq id id' -> true
| _ :: sign -> mem_named_context id sign
| [] -> false
let clear_named_body id env =
let aux _ = function
- | (id',Some c,t) when id = id' -> push_named (id,None,t)
+ | (id',Some c,t) when id_eq id id' -> push_named (id,None,t)
| d -> push_named d in
fold_named_context aux env ~init:(reset_context env)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index b6bb438680..4d9ce49690 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -103,7 +103,6 @@ exception Occur
val occur_meta : types -> bool
val occur_existential : types -> bool
val occur_meta_or_existential : types -> bool
-val occur_const : constant -> types -> bool
val occur_evar : existential_key -> types -> bool
val occur_var : env -> identifier -> types -> bool
val occur_var_in_decl :
@@ -199,7 +198,6 @@ val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
val eta_reduce_head : constr -> constr
-val eta_eq_constr : constr -> constr -> bool
exception CannotFilter
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 95fdcdfe69..7d9d0bbd8b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -140,7 +140,11 @@ let rec is_class_type evd c =
match kind_of_term c with
| Prod (_, _, t) -> is_class_type evd t
| Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
- | _ -> class_of_constr c <> None
+ | _ ->
+ begin match class_of_constr c with
+ | Some _ -> true
+ | None -> false
+ end
let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
@@ -324,7 +328,7 @@ let discharge_instance (_, (action, inst)) =
is_impl = Lib.discharge_global inst.is_impl })
-let is_local i = i.is_global = -1
+let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
@@ -333,7 +337,10 @@ let add_instance check inst =
(Global.env ()) Evd.empty inst.is_impl inst.is_pri)
let rebuild_instance (action, inst) =
- if action = AddInstance then add_instance true inst;
+ let () = match action with
+ | AddInstance -> add_instance true inst
+ | _ -> ()
+ in
(action, inst)
let classify_instance (action, inst) =
@@ -415,13 +422,20 @@ let add_inductive_class ind =
*)
let instance_constructor cl args =
- let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
+ let filter (_, b, _) = match b with
+ | None -> true
+ | Some _ -> false
+ in
+ let lenpars = List.length (List.filter filter (snd cl.cl_context)) in
let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
| IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
applistc (mkInd ind) pars
| ConstRef cst ->
- let term = if args = [] then None else Some (List.last args) in
+ let term = match args with
+ | [] -> None
+ | _ -> Some (List.last args)
+ in
term, applistc (mkConst cst) pars
| _ -> assert false
@@ -441,7 +455,7 @@ let instances r =
let cl = class_info r in instances_of cl
let is_class gr =
- Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
+ Gmap.fold (fun k v acc -> acc || eq_gr v.cl_impl gr) !classes false
let is_instance = function
| ConstRef c ->
@@ -456,7 +470,9 @@ let is_instance = function
is_class (IndRef ind)
| _ -> false
-let is_implicit_arg k = k <> Evar_kinds.GoalEvar
+let is_implicit_arg = function
+| Evar_kinds.GoalEvar -> false
+| _ -> true
(* match k with *)
(* ImplicitArg (ref, (n, id), b) -> true *)
(* | InternalHole -> true *)
@@ -476,7 +492,7 @@ let resolvable = Store.field ()
open Store.Field
let is_resolvable evi =
- assert (evi.evar_body = Evar_empty);
+ assert (match evi.evar_body with Evar_empty -> true | _ -> false);
Option.default true (resolvable.get evi.evar_extra)
let mark_resolvability_undef b evi =
@@ -484,7 +500,7 @@ let mark_resolvability_undef b evi =
{ evi with evar_extra = t }
let mark_resolvability b evi =
- assert (evi.evar_body = Evar_empty);
+ assert (match evi.evar_body with Evar_empty -> true | _ -> false);
mark_resolvability_undef b evi
let mark_unresolvable evi = mark_resolvability false evi
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b24992b8d7..09ba88bb9d 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -64,7 +64,7 @@ let e_judge_of_apply env evdref funj argjv =
apply_rec 1 funj.uj_type (Array.to_list argjv)
let e_check_branch_types env evdref ind cj (lfj,explft) =
- if Array.length lfj <> Array.length explft then
+ if not (Int.equal (Array.length lfj) (Array.length explft)) then
error_number_branches env cj (Array.length explft);
for i = 0 to Array.length explft - 1 do
if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
@@ -124,7 +124,7 @@ let check_allowed_sort env sigma ind c p =
let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
let specif = Global.lookup_inductive ind in
let sorts = elim_sorts specif in
- if not (List.exists ((=) ksort) sorts) then
+ if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
error_elim_arity env ind sorts c pj
(Some(ksort,s,error_elim_explain ksort s))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 856c5e1477..bf0f47a32c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -40,7 +40,7 @@ let occur_meta_evd sigma mv c =
(* Note: evars are not instantiated by terms with metas *)
let c = whd_evar sigma (whd_meta sigma c) in
match kind_of_term c with
- | Meta mv' when mv = mv' -> raise Occur
+ | Meta mv' when Int.equal mv mv' -> raise Occur
| _ -> iter_constr occrec c
in try occrec c; false with Occur -> true
@@ -116,7 +116,7 @@ let pose_all_metas_as_evars env evd t =
| Some ({rebus=c},_) -> c
| None ->
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
- let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
+ let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let ev = Evarutil.e_new_evar evdref env ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in
evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
ev)
@@ -380,7 +380,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
and cN = Evarutil.whd_head_evar sigma curn in
match (kind_of_term cM,kind_of_term cN) with
| Meta k1, Meta k2 ->
- if k1 = k2 then substn else
+ if Int.equal k1 k2 then substn else
let stM,stN = extract_instance_status pb in
if wt && flags.check_applied_meta_types then
(let tyM = Typing.meta_type sigma k1 in
@@ -431,7 +431,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
| Sort s1, Sort s2 ->
(try
let sigma' =
- if cv_pb = CUMUL
+ if cv_pb == CUMUL
then Evd.set_leq_sort sigma s1 s2
else Evd.set_eq_sort sigma s1 s2
in (sigma', metasubst, evarsubst)
@@ -605,8 +605,11 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- if flags.modulo_conv_on_closed_terms = None ||
- subterm_restriction b flags then
+ if
+ begin match flags.modulo_conv_on_closed_terms with
+ | None -> true
+ | Some _ -> subterm_restriction b flags
+ end then
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else
try f1 () with e when precatchable_exception e ->
@@ -626,7 +629,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
let (evd,ks,_) =
List.fold_left
(fun (evd,ks,m) b ->
- if m=n then (evd,t2::ks, m-1) else
+ if Int.equal m n then (evd,t2::ks, m-1) else
let mv = new_meta () in
let evd' = meta_declare mv (substl ks b) evd in
(evd', mkMeta mv :: ks, m - 1))
@@ -704,14 +707,14 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
| ((IsSubType | Conv as oppst1),
(IsSubType | Conv)) ->
let res = unify_0 env sigma CUMUL flags c2 c1 in
- if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
- else if st2=IsSubType then (left, st1, res)
+ if eq_instance_constraint oppst1 st2 then (* arbitrary choice *) (left, st1, res)
+ else if eq_instance_constraint st2 IsSubType then (left, st1, res)
else (right, st2, res)
| ((IsSuperType | Conv as oppst1),
(IsSuperType | Conv)) ->
let res = unify_0 env sigma CUMUL flags c1 c2 in
- if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
- else if st2=IsSuperType then (left, st1, res)
+ if eq_instance_constraint oppst1 st2 then (* arbitrary choice *) (left, st1, res)
+ else if eq_instance_constraint st2 IsSuperType then (left, st1, res)
else (right, st2, res)
| (IsSuperType,IsSubType) ->
(try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
@@ -832,9 +835,10 @@ let unify_type env sigma flags mv status c =
let order_metas metas =
let rec order latemetas = function
| [] -> List.rev latemetas
- | (_,_,(status,to_type) as meta)::metas ->
- if to_type = CoerceToType then order (meta::latemetas) metas
- else meta :: order latemetas metas
+ | (_,_,(_,CoerceToType) as meta)::metas ->
+ order (meta::latemetas) metas
+ | (_,_,(_,_) as meta)::metas ->
+ meta :: order latemetas metas
in order [] metas
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
@@ -886,13 +890,15 @@ let w_merge env with_types flags (evd,metas,evars) =
match metas with
| (mv,c,(status,to_type))::metas ->
let ((evd,c),(metas'',evars'')),eqns =
- if with_types & to_type <> TypeProcessed then
- if to_type = CoerceToType then
+ if with_types && to_type != TypeProcessed then
+ begin match to_type with
+ | CoerceToType ->
(* Some coercion may have to be inserted *)
(w_coerce env evd mv c,([],[])),eqns
- else
+ | _ ->
(* No coercion needed: delay the unification of types *)
((evd,c),([],[])),(mv,status,c)::eqns
+ end
else
((evd,c),([],[])),eqns
in
@@ -1010,7 +1016,7 @@ let w_typed_unify_list env evd flags f1 l1 f2 l2 =
let iter_fail f a =
let n = Array.length a in
let rec ffail i =
- if i = n then error "iter_fail"
+ if Int.equal i n then error "iter_fail"
else
try f a.(i)
with ex when precatchable_exception ex -> ffail (i+1)
@@ -1096,7 +1102,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) =
let bind_iter f a =
let n = Array.length a in
let rec ffail i =
- if i = n then fun a -> a
+ if Int.equal i n then fun a -> a
else bind (f a.(i)) (ffail (i+1))
in ffail 0
in
@@ -1135,10 +1141,10 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) =
| _ -> fail "Match_subterm"))
in
let res = matchrec cl [] in
- if res = [] then
+ match res with
+ | [] ->
raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
- else
- res
+ | _ -> res
let w_unify_to_subterm_list env evd flags hdmeta oplist t =
List.fold_right
@@ -1223,10 +1229,12 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
let hd1,l1 = whd_nored_stack evd ty1 in
let hd2,l2 = whd_nored_stack evd ty2 in
- match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
+ let is_empty1 = match l1 with [] -> true | _ -> false in
+ let is_empty2 = match l2 with [] -> true | _ -> false in
+ match kind_of_term hd1, not is_empty1, kind_of_term hd2, not is_empty2 with
(* Pattern case *)
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
- when List.length l1 = List.length l2 ->
+ when Int.equal (List.length l1) (List.length l2) ->
(try
w_typed_unify_list env evd flags hd1 l1 hd2 l2
with ex when precatchable_exception ex ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:06:29 +0000