+let letin term =
+ let module C = Cic in
+ let curi,metasenv,pbo,pty =
+ match !proof with
+ None -> assert false
+ | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let (metano,context,ty) =
+ match !goal with
+ None -> assert false
+ | Some (metano,(context,ty)) -> metano,context,ty
+ in
+ let ciccontext = cic_context_of_named_context context in
+ let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
+ let newmeta = new_meta () in
+ let newmetaty = CicSubstitution.lift 1 ty in
+ let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
+ refine_meta metano bo' [newmeta,newmetaty];
+ goal :=
+ Some
+ (newmeta,
+ ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
+;;
+