From 08f7d8d83fd0a5f18ae764a21a21b5336a0ce7f5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 19 May 2007 21:13:42 +0000
Subject: Backtrack sur l'effacement dans le contexte de but des lieurs
 apparaissant sans nom dans "refine" (quelques incompatibilités, par exemple
 dans les preuves de Lannion/continuations/Nxaccu_ex.core_V1,
 Bordeaux/Additions/log2_spec.ceiling_log2, et
 Bordeaux/NewSearchTree/search_tree.rm).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9841 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/refine.ml | 28 ++++++++--------------------
 1 file changed, 8 insertions(+), 20 deletions(-)

diff --git a/tactics/refine.ml b/tactics/refine.ml
index a9fdfacb89..3dc8294627 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -148,26 +148,14 @@ let rec compute_metamap env sigma c = match kind_of_term c with
   | Lambda (name,c1,c2) ->
       let v = fresh env name in
       let env' = push_named (v,None,c1) env in
-      let allow_anon_vars_in_evars = false in
-      if allow_anon_vars_in_evars or name<>Anonymous or dependent (mkRel 1) c2
-      then
-        begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
-	  (* terme de preuve complet *)
-	  | TH (_,_,[]) -> TH (c,[],[])
-	  (* terme de preuve incomplet *)    
-	  | th ->
-	      let m,mm,sgp = replace_by_meta env' sigma th in
-	      TH (mkLambda (Name v,c1,m), mm, sgp)
-        end
-      else
-        begin match compute_metamap env' sigma c2 with
-	  (* terme de preuve complet *)
-	  | TH (_,_,[]) -> TH (c,[],[])
-	  (* terme de preuve incomplet *)    
-	  | th ->
-	      let m,mm,sgp = replace_by_meta env' sigma th in
-	      TH (mkLambda (Anonymous,c1,m), mm, sgp)
-        end
+      begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
+	(* terme de preuve complet *)
+	| TH (_,_,[]) -> TH (c,[],[])
+	(* terme de preuve incomplet *)    
+	| th ->
+	    let m,mm,sgp = replace_by_meta env' sigma th in
+	    TH (mkLambda (Name v,c1,m), mm, sgp)
+      end
 
   | LetIn (name, c1, t1, c2) ->
       let v = fresh env name in
-- 
cgit v1.2.3