diff options
| -rw-r--r-- | pretyping/evarutil.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 5 | ||||
| -rw-r--r-- | proofs/goal.ml | 7 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 |
4 files changed, 28 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index dd74ecf38..0fcff3d49 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -656,6 +656,18 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c +(* spiwack: this is a more complete version of + {!Termops.occur_evar}. The latter does not look recursively into an + [evar_map]. If unification only need to check superficially, tactics + do not have this luxury, and need the more complete version. *) +let occur_evar_upto sigma n c = + let rec occur_rec c = match kind_of_term c with + | Evar (sp,_) when Evar.equal sp n -> raise Occur + | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) + | _ -> iter_constr occur_rec c + in + try occur_rec c; false with Occur -> true + (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index ea00f8067..8e8bbf367 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -132,6 +132,11 @@ val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t +(** [occur_evar_upto sigma k c] returns [true] if [k] appears in + [c]. It looks up recursively in [sigma] for the value of existential + variables. *) +val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool + (** {6 Value/Type constraints} *) val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment diff --git a/proofs/goal.ml b/proofs/goal.ml index ef71dd04c..fe8018e47 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -81,12 +81,17 @@ module V82 = struct (* Instantiates a goal with an open term *) let partial_solution sigma evk c = + (* Check that the goal itself does not appear in the refined term *) + let _ = + if not (Evarutil.occur_evar_upto sigma evk c) then () + else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + in Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = let id = Evd.evar_ident evk sigma in - Evd.rename evk' id (Evd.define evk c sigma) + Evd.rename evk' id (partial_solution sigma evk c) (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 82dd9f6e7..08a43737c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -978,6 +978,11 @@ struct let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in (** Check that the refined term is typesafe *) let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + (** Check that the goal itself does not appear in the refined term *) + let _ = + if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then () + else Pretype_errors.error_occur_check env sigma gl.Goal.self c + in (** Proceed to the refinement *) let sigma = match evkmain with | None -> Evd.define gl.Goal.self c sigma |