+
+(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
+
+module C = Cic
+
+let letout_tac =
+ let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
+ let term = C.Sort C.Set in
+ let letout_tac (proof, goal) =
+ let curi, metasenv, pbo, pty = proof in
+ let metano, context, ty = CicUtil.lookup_meta goal metasenv in
+ let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
+ let context_for_newmeta = None :: context in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
+ let newmetaty = CicSubstitution.lift 1 ty in
+ let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
+ let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+ newproof, [newmeta]
+ in
+ mk_tactic letout_tac