From fa1cb4a55262a1dced369ae6556265b968f4b9a3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Oct 2016 19:35:16 +0200
Subject: Fixing to #3209 (Not_found due to an occur-check cycle).

The fix solves the original bug report but it only turns the Not_found
into a normal error in the alternative example by Guillaume. See
test-suite file for comments on how to eventually improve the
situation and find a solution in Guillaume's example too.
---
 pretyping/evarsolve.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4084ee579a..4a99246bba 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -600,7 +600,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
  * substitution u1..uq.
  *)
 
+exception MorePreciseOccurCheckNeeeded
+
 let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+  if Evd.is_defined evd evk1 then
+      (* Some circularity somewhere (see e.g. #3209) *)
+      raise MorePreciseOccurCheckNeeeded;
+  let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
   let evi1 = Evd.find_undefined evd evk1 in
   let env1,rel_sign = env_rel_context_chop k env in
   let sign1 = evar_hyps evi1 in
@@ -1542,6 +1548,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         postpone_non_unique_projection env evd pbty ev sols rhs
     | NotEnoughInformationEvarEvar t ->
         add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+    | MorePreciseOccurCheckNeeeded ->
+        add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
     | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
         raise e
     | OccurCheckIn (evd,rhs) ->
-- 
cgit v1.2.3