diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-19 21:13:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-19 21:13:42 +0000 |
| commit | 08f7d8d83fd0a5f18ae764a21a21b5336a0ce7f5 (patch) | |
| tree | c003d1a28d151049892d4a22c0c31061944c9a9d /tactics | |
| parent | 54ac5f1369e82b9c72b7f6a2ed0a9cf3dc02ddcf (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/refine.ml | 28 |
1 files changed, 8 insertions, 20 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index a9fdfacb8..3dc829462 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 |