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.

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 110e882af2b02c51752ef2411e41f1c60c5047e4..8d07811ea3333d450caf68f347e39f1b6a1772e6 100644 (file)
--- 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 ->