TacticErrors (rocq-runtime.TacticErrors)

Raising exceptions.

val intro_already_declared : ?loc:Loc.t -> Names.Id.t -> 'a

val clear_dependency : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t option -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> 'a

val replacing_dependency : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> 'a

val already_used : ?loc:Loc.t -> Names.Id.t -> 'a

val used_twice : ?loc:Loc.t -> Names.Id.t -> 'a

val variable_has_no_value : ?loc:Loc.t -> Names.Id.t -> 'a

val convert_incompatible_types : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'a

val convert_not_a_type : ?loc:Loc.t -> unit -> 'a

val not_convertible : ?loc:Loc.t -> unit -> 'a

val not_unfoldable : ?loc:Loc.t -> unit -> 'a

val no_quantified_hypothesis : ?loc:Loc.t -> Tactypes.quantified_hypothesis -> bool -> 'a

val cannot_find_instance : ?loc:Loc.t -> Names.Id.t -> 'a

val nothing_to_rewrite : ?loc:Loc.t -> Names.Id.t -> 'a

val ill_formed_elimination_type : ?loc:Loc.t -> unit -> 'a

val unable_to_apply_lemma : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'a

val depends_on_body : ?loc:Loc.t -> Names.Id.t list -> Names.Id.Set.t -> Names.Id.t option -> 'a

val not_right_number_constructors : ?loc:Loc.t -> int -> 'a

val not_enough_constructors : ?loc:Loc.t -> unit -> 'a

val constructors_numbered_from_one : ?loc:Loc.t -> unit -> 'a

val no_constructors : ?loc:Loc.t -> unit -> 'a

val unexpected_extra_pattern : ?loc:Loc.t -> int option -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr -> 'a

val cannot_find_inductive_argument : ?loc:Loc.t -> unit -> 'a

val one_intro_pattern_expected : ?loc:Loc.t -> unit -> 'a

val keep_and_clear_modifier_only_for_hypotheses : ?loc:Loc.t -> unit -> 'a

val fixpoint_on_non_inductive_type : ?loc:Loc.t -> unit -> 'a

val not_enough_products : ?loc:Loc.t -> unit -> 'a

val all_methods_in_coinductive_type : ?loc:Loc.t -> unit -> 'a

val replacement_ill_typed : ?loc:Loc.t -> exn -> 'a

val not_enough_premises : ?loc:Loc.t -> unit -> 'a

val need_dependent_product : ?loc:Loc.t -> unit -> 'a

Internal use only.

val clear_dependency_msg : Environ.env -> Evd.evar_map -> Names.Id.t option -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> Pp.t

exception NotConvertible

exception DependsOnBody of Names.Id.t list * Names.Id.Set.t * Names.Id.t option