Ltac2_plugin.Tac2interptype environment = Tac2env.environmentval empty_environment : environmentval interp : environment -> Tac2expr.glb_tacexpr -> Tac2val.valexpr Proofview.tacticval interp_value : environment -> Tac2expr.glb_tacexpr -> Tac2val.valexprSame as interp but assumes that the argument is a syntactic value.
val eval_global : Tac2expr.ltac_constant -> Tac2val.valexprval eval_glb_ext : environment -> Tac2dyn.Arg.glb -> Tac2val.valexpr Proofview.tacticval push_id : environment -> Names.Id.t -> Tac2val.valexpr -> environmentval get_env : Ltac_pretype.unbound_ltac_var_map -> environmentval set_env : environment -> Ltac_pretype.unbound_ltac_var_map -> Ltac_pretype.unbound_ltac_var_mapexception LtacError of Names.KerName.t * Tac2val.valexpr arrayLtac2-defined exceptions seen from OCaml side