Ajout du langage de tactiques

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

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 94f69474b7..91a83ea9d9 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Evd
 open Reduction
 open Typing
 open Proof_trees
+open Proof_type
 open Logic
 open Refiner
 
@@ -58,7 +59,6 @@ let extract_decl sp evc =
 
 let restore_decl sp evd evc =
   let newctxt = { lc = (ts_it evc).focus;
-                  mimick = (get_mimick evd);
                   pgm = (get_pgm evd) } in
   let newgoal = { evar_env = evd.evar_env; 
 		  evar_concl = evd.evar_concl;