From 456c7abfc921d9f1f5dcd0107f81b48d71f7f92e Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 7 Jul 2004 13:06:04 +0000
Subject: bypass w_Define when w_refine-ing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5868 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 719d95aedc..4f644ac4e4 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -141,7 +141,9 @@ let w_refine ev rawc wc =
   let evd,typed_c = 
     Pretyping.understand_gen_tcc wc.sigma env [] 
       (Some e_info.evar_concl) rawc in
-    w_Define ev typed_c {wc with sigma=evd}
+  let inst_info = {e_info with evar_body = Evar_defined typed_c } in
+    restore_decl ev inst_info (extract_decl ev {wc with sigma=evd})
+ (*   w_Define ev typed_c {wc with sigma=evd} *)
 
 (* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
 
-- 
cgit v1.2.3