diff options
| author | Arnaud Spiwack | 2014-12-04 13:15:26 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-04 14:38:05 +0100 |
| commit | 964024bf87a87b0e87d8891b3090083ea49b1d03 (patch) | |
| tree | 0d10a2a7e4961be66f3a925b0765b8d42cbdef0f /proofs | |
| parent | f66b84de608830600e43f6d1a97c29226b6b58ea (diff) | |
Occur-check in refine.
The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].
I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.
The same check is done in the compatibility layer.
Fixes a reported bug which I cannot locate for some reason.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 7 | ||||
| -rw-r--r-- | proofs/proofview.ml | 5 |
2 files changed, 11 insertions, 1 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ef71dd04c8..fe8018e47b 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 82dd9f6e77..08a43737c4 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 |