From 3f40ddb52ed52ea1e1939feaecf952269335500f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 25 Apr 2009 17:41:20 +0000
Subject: - Fixing #2090 (occur check missing when trying to solve evar-evar
 equation). - Adding test file related to commit 12080 (bug #2091). - Cleaning
 old parsing stuff from 8.0. - Support for camlp5 in base_include.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1a7bb2c6cf..e7682285b9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -659,7 +659,11 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
 
 let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
   let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
-  invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders
+  let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+  match res with
+  | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
+  | _ -> res
+
 
 let effective_projections =
   map_succeed (function Invertible c -> c | _ -> failwith"")
-- 
cgit v1.2.3