From c6763b44c75b2bd9aebdbcd0798287c90431cde4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Jul 2012 05:14:44 +0000
Subject: Fixing #2836 (materialize_evar might refine as a side effect the
 current evar to project; this may happen if this evar is dependent and is
 involved in evar-evar conversion problem eventually solved by instantiating
 the current evar; could maybe be optimized when the evar to materialize has
 invertible instance in which case define_evar_from_virtual_equation applied
 on the current evar could be shortcut, avoiding to create an evar).

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

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 036bed5252..a2c63982bc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -146,6 +146,11 @@ let noccur_evar evd evk c =
   in
   try occur_rec c; true with Occur -> false
 
+let normalize_evar evd ev =
+  match kind_of_term (whd_evar evd (mkEvar ev)) with
+  | Evar (evk,args) -> (evk,args)
+  | _ -> assert false
+
 (**********************)
 (* Creating new metas *)
 (**********************)
@@ -1591,6 +1596,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
 	  let ty = get_type_of env' !evdref t in
 	  let (evd,evar'',ev'') =
              materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+          (* materialize_evar may instantiate ev' by another evar; adjust it *)
+          let (evk',args' as ev') = normalize_evar evd ev' in
 	  let evd =
 	     (* Try to project (a restriction of) the left evar ... *)
 	    try
-- 
cgit v1.2.3