From b4c775bb0a5efda8d3c94c21cf07e9ead7282785 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Apr 2009 16:16:59 +0000 Subject: [PATCH] Bug fixed in two lines + 5 lines of comment. During select, the context of the goal is changed and the conclusion is changed too (too a ?[out_scope]). Then the changed conclusion was relocated in the changed context, triggering a delift that in turn triggered the unification case "something vs ?[out_of_scope]"... at the bad time! Fixed by manually relocating the new conclusion in the new context. Manually means opening and building again the cic_term data type, which is ugly and sort of fragile. --- helm/software/components/ng_tactics/nTactics.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 110e882af..8d07811ea 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -274,9 +274,6 @@ let select0_tac ~where:(wanted,hyps,where) ~job = let path = match where with None -> NCic.Implicit `Term | Some where -> where in - let status, newgoalty = - select_term status ~found ~postprocess goalty (wanted,path) - in let status, newgoalctx = List.fold_right (fun (name,d as entry) (status,ctx) -> @@ -299,6 +296,16 @@ let select0_tac ~where:(wanted,hyps,where) ~job = Not_found -> status, entry::ctx ) (ctx_of goalty) (status,[]) in + let status, newgoalty = + select_term status ~found ~postprocess goalty (wanted,path) in + (* WARNING: the next two lines simply change the context of newgoalty + from the old to the new one. Otherwise mk_meta will do that herself, + calling relocate that calls delift. However, newgoalty is now + ?[out_scope] and thus the delift would trigger the special unification + case, which is wrong now :-( *) + let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in + let newgoalty = mk_cic_term newgoalctx newgoalty in + let status, instance = mk_meta status newgoalctx (`Decl newgoalty) in @@ -494,7 +501,7 @@ let case1_tac name = cases_tac ~where:("",0,(None,[],None)) ~what:("",0,Ast.Ident (name,None)); - if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] + if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] ;; let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> -- 2.39.2