From 964024bf87a87b0e87d8891b3090083ea49b1d03 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 4 Dec 2014 13:15:26 +0100
Subject: 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.
---
 proofs/goal.ml      | 7 ++++++-
 proofs/proofview.ml | 5 +++++
 2 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3