Fixing bug 1795 (occur check was not correctly done)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10551 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 62bb7ef26..950016540 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -860,8 +860,6 @@ let rec invert_instance env evd (evk,_ as ev) subst rhs =
  *)
 
 and evar_define env (evk,argsv as ev) rhs evd =
-  if occur_evar evk rhs
-  then error_occur_check env (evars_of evd) evk rhs;
   let evi = Evd.find (evars_of evd) evk in
   (* the bindings to invert *)
   let subst = make_projectable_subst (evars_of evd) evi argsv in
@@ -869,6 +867,8 @@ and evar_define env (evk,argsv as ev) rhs evd =
     let (evd',body) = invert_instance env evd ev subst rhs in
     if occur_meta body then error "Meta cannot occur in evar body"
     else
+      if occur_evar evk body
+      then error_occur_check env (evars_of evd) evk body;
       (* needed only if an inferred type *)
       let body = refresh_universes body in
 (* Cannot strictly type instantiations since the unification algorithm
@@ -941,6 +941,8 @@ let solve_pattern_eqn env l1 c =
       | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
       | _ -> assert false) 
     l1 c in
+  (* Warning: we may miss some opportunity to eta-reduce more since c'
+     is not in normal form *)
   whd_eta c'
 
 (* This code (i.e. solve_pb, etc.) takes a unification