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.

1 files changed, 5 insertions, 0 deletions

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