diff options
| -rw-r--r-- | pretyping/termops.ml | 5 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 | ||||
| -rw-r--r-- | pretyping/unification.ml | 28 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 |
4 files changed, 31 insertions, 8 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 67559e686..c68f2c4d9 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -575,6 +575,11 @@ let dependent_no_evar = dependent_main true false let dependent_univs = dependent_main false true let dependent_univs_no_evar = dependent_main true true +let dependent_in_decl a (_,c,t) = + match c with + | None -> dependent a t + | Some body -> dependent a body || dependent a t + let count_occurrences m t = let n = ref 0 in let rec countrec m t = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 72a115231..ebcf4285c 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -110,6 +110,7 @@ val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val dependent_univs : constr -> constr -> bool val dependent_univs_no_evar : constr -> constr -> bool +val dependent_in_decl : constr -> named_declaration -> bool val count_occurrences : constr -> constr -> int val collect_metas : constr -> int list val collect_vars : constr -> Id.Set.t (** for visible vars only *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index dbdc0a4e4..9baabae77 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -7,6 +7,7 @@ (************************************************************************) open Errors +open Pp open Util open Names open Term @@ -1180,6 +1181,17 @@ let occurrences_of_goal cls = let in_every_hyp cls = Option.is_empty cls.onhyps +let indirectly_dependent c d decls = + not (isVar c) && + (* This test is not needed if the original term is a variable, but + 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 (id,_,_) -> dependent_in_decl (mkVar id) d) decls + +let indirect_dependency d decls = + pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls)) + let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) = let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma in Evd.evar_universe_context sigma, nf_evar sigma c @@ -1250,10 +1262,20 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with - | None -> depdecls + | None -> + if indirectly_dependent c d depdecls then + (* Told explicitly not to abstract over [d], but it is dependent *) + let id' = indirect_dependency d depdecls in + errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' + ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp + ++ str ".") + else + depdecls | Some ((AllOccurrences, InHyp) as occ) -> let newdecl = subst_closed_term_occ_decl_modulo occ test d in - if Context.eq_named_declaration d newdecl then + if Context.eq_named_declaration d newdecl + && not (indirectly_dependent c d depdecls) + then if check_occs && not (in_every_hyp occs) then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp))) else depdecls @@ -1280,7 +1302,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc or pattern at some occurrences; it returns: - the id used for the abstraction - the type of the abstraction - - the hypotheses from the context which depend on the term or pattern + - the declarations from the context which depend on the term or pattern - the most recent hyp before which there is no dependency in the term of pattern - the abstracted conclusion - an evar universe context effect to apply on the goal diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 450b48d45..30568edab 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -660,11 +660,6 @@ let rec intros_move = function Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false) (intros_move rest) -let dependent_in_decl a (_,c,t) = - match c with - | None -> dependent a t - | Some body -> dependent a body || dependent a t - (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) |