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.
let path =
match where with None -> NCic.Implicit `Term | Some where -> where
in
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) ->
let status, newgoalctx =
List.fold_right
(fun (name,d as entry) (status,ctx) ->
Not_found -> status, entry::ctx
) (ctx_of goalty) (status,[])
in
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
let status, instance =
mk_meta status newgoalctx (`Decl newgoalty)
in
cases_tac
~where:("",0,(None,[],None))
~what:("",0,Ast.Ident (name,None));
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 ->
;;
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->