diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 18 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 15 | ||||
| -rw-r--r-- | pretyping/unification.ml | 7 |
3 files changed, 23 insertions, 17 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 73be9d6b7..de2e735c7 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 @@ -1936,8 +1938,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. *) -> @@ -1948,13 +1950,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 96d80741a..484ecea7e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -527,7 +527,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 -> @@ -1072,8 +1072,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 *) @@ -1081,9 +1087,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 f2f922fd5..7d5688f7b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -699,7 +699,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 @@ -719,7 +719,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 @@ -1506,7 +1506,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 |