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