tac2core.ml

(* next to constr_in_context *)

let () =
  define "constr_in_context_alt" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c ->
  Proofview.Goal.goals >>= function
  | [gl] ->
    gl >>= fun gl ->
    let env = Proofview.Goal.env gl in
    let sigma = Proofview.Goal.sigma gl in
    let has_var =
      try
        let _ = Environ.lookup_named id env in
        true
      with Not_found -> false
    in
    if has_var then
      Tacticals.tclZEROMSG (str "Variable already exists")
    else
      let open Context.Named.Declaration in
      let sigma, t_rel =
        let t_ty = Retyping.get_type_of env sigma t in
        (* If the user passed eg ['_] for the type we force it to indeed be a type *)
        let sigma, j = Typing.type_judgment env sigma {uj_val=t; uj_type=t_ty} in
        sigma, EConstr.ESorts.relevance_of_sort j.utj_type
      in
      let nenv = EConstr.push_named (LocalAssum (Context.make_annot id t_rel, t)) env in
      let unit_t = Coqlib.lib_ref "core.unit.type" in
      let sigma, unit_t = Evd.fresh_global nenv sigma unit_t in
      let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma unit_t in
      Proofview.Unsafe.tclEVARS sigma >>= fun () ->
      Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state evk] >>= fun () ->
      thaw c >>= fun c ->
      Proofview.Unsafe.tclSETGOALS [Proofview.with_empty_state (Proofview.Goal.goal gl)] >>= fun () ->
      let sigma, tt_v = Evd.fresh_global nenv sigma @@ Coqlib.lib_ref "core.unit.tt" in
      let sigma = Evd.define evk tt_v sigma in
      let c = to_constr c in
      let c = EConstr.Vars.subst_var sigma id c in
      Proofview.Unsafe.tclEVARS sigma <*>
      return (EConstr.mkLambda (Context.make_annot (Name id) t_rel, t, c))
  | _ ->
    throw err_notfocussed