aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/termops.ml7
-rw-r--r--engine/termops.mli1
-rw-r--r--plugins/firstorder/unify.ml4
-rw-r--r--pretyping/cases.ml18
-rw-r--r--pretyping/evarsolve.ml15
-rw-r--r--pretyping/unification.ml7
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/inv.ml2
8 files changed, 36 insertions, 22 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 51fc59289..0c567754a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -857,6 +857,13 @@ let occur_meta_or_existential sigma c =
| _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
+let occur_metavariable sigma m c =
+ let rec occrec c = match EConstr.kind sigma c with
+ | Meta m' -> if Int.equal m m' then raise Occur
+ | _ -> EConstr.iter sigma occrec c
+ in
+ try occrec c; false with Occur -> true
+
let occur_evar sigma n c =
let rec occur_rec c = match EConstr.kind sigma c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
diff --git a/engine/termops.mli b/engine/termops.mli
index bb3cbb6a8..6e63539ca 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -94,6 +94,7 @@ exception Occur
val occur_meta : Evd.evar_map -> constr -> bool
val occur_existential : Evd.evar_map -> constr -> bool
val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_in_decl :
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 06f56d06e..d63fe9d79 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -56,12 +56,12 @@ let unif evd t1 t2=
| Meta i,_ ->
let t=subst_meta !sigma nt2 in
if Int.Set.is_empty (free_rels evd t) &&
- not (dependent evd (EConstr.mkMeta i) t) then
+ not (occur_metavariable evd i t) then
bind i t else raise (UFAIL(nt1,nt2))
| _,Meta i ->
let t=subst_meta !sigma nt1 in
if Int.Set.is_empty (free_rels evd t) &&
- not (dependent evd (EConstr.mkMeta i) t) then
+ not (occur_metavariable evd i t) then
bind i t else raise (UFAIL(nt1,nt2))
| Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
| _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ee7c39982..38196489a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -574,7 +574,7 @@ let dependent_decl sigma a =
let rec dep_in_tomatch sigma n = function
| (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l
- | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l
+ | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l
| [] -> false
let dependencies_in_rhs sigma nargs current tms eqns =
@@ -1704,9 +1704,11 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
List.map_i
(fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
(rel_context extenv) in
- let rel_filter =
- List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u
- || Int.Set.mem (destRel !evdref a) depvl) inst in
+ let map a = match EConstr.kind !evdref a with
+ | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl
+ | _ -> true
+ in
+ let rel_filter = List.map map inst in
let named_filter =
List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
(named_context extenv) in
@@ -1937,8 +1939,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match EConstr.kind sigma tm with
- | Rel n when dependent sigma tm c
- && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
+ | Rel n when Int.equal signlen 1 && not (noccurn sigma n c)
+ (* The term to match is not of a dependent type itself *) ->
((n, len) :: subst, len - signlen)
| Rel n when signlen > 1 (* The term is of a dependent type,
maybe some variable in its type appears in the tycon. *) ->
@@ -1949,13 +1951,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_left
(fun (subst, len) arg ->
match EConstr.kind sigma arg with
- | Rel n when dependent sigma arg c ->
+ | Rel n when not (noccurn sigma n c) ->
((n, len) :: subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent sigma tm c && List.for_all (isRel sigma) realargs
+ if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs
then (n, len) :: subst else subst
in (subst, pred len))
| _ -> (subst, len - signlen))
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7eaff078..aefae1ecc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -525,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t =
match Option.List.map map l with
| Some l ->
begin match find_unification_pattern_args env evd l t with
- | Some _ as x when not (dependent evd (mkMeta m) t) -> x
+ | Some _ as x when not (occur_metavariable evd m t) -> x
| _ -> None
end
| None ->
@@ -1068,8 +1068,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
let rhs = expand_vars_in_term env evd rhs in
- let filter =
- restrict_upon_filter evd evk
+ let filter a = match EConstr.kind evd a with
+ | Rel n -> not (noccurn evd n rhs)
+ | Var id ->
+ local_occur_var evd id rhs
+ || List.exists (fun (id', _) -> Id.equal id id') sols
+ | _ -> true
+ in
+ let filter = restrict_upon_filter evd evk filter argsv in
(* Keep only variables that occur in rhs *)
(* This is not safe: is the variable is a local def, its body *)
(* may contain references to variables that are removed, leading to *)
@@ -1077,9 +1083,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
(* that says that the body is hidden. Note that expand_vars_in_term *)
(* expands only rels and vars aliases, not rels or vars bound to an *)
(* arbitrary complex term *)
- (fun a -> not (isRel evd a || isVar evd a)
- || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols)
- argsv in
let filter = closure_of_filter evd evk filter in
let candidates = extract_candidates sols in
match candidates with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b9678fa10..b49291adb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -698,7 +698,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
else sigma,(k2,cM,stM)::metasubst,evarsubst
| Meta k, _
- when not (dependent sigma cM cN) (* helps early trying alternatives *) ->
+ when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
@@ -718,7 +718,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cN)
| _, Meta k
- when not (dependent sigma cN cM) (* helps early trying alternatives *) ->
+ when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) ->
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
@@ -1500,7 +1500,8 @@ let indirectly_dependent sigma c d decls =
it is needed otherwise, as e.g. when abstracting over "2" in
"forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
way to see that the second hypothesis depends indirectly over 2 *)
- List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
+ let open Context.Named.Declaration in
+ List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f9e06391a..d7e697aed 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1808,9 +1808,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+ | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+ | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 28cfd57a2..339abbc2e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names =
make_inv_predicate env evdref indf realargs id status concl in
let sigma = !evdref in
let (cut_concl,case_tac) =
- if status != NoDep && (dependent sigma c concl) then
+ if status != NoDep && (local_occur_var sigma id concl) then
Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
case_then_using
else
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 11:01:28 +0000