package rocq-runtime

  1. Overview
  2. Docs

Module TacticErrorsSource

Common exceptions raised by tactics. These exceptions are catched at toplevel and pretty-printed to the user.

Raising exceptions.
Sourceval intro_already_declared : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval clear_dependency : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t option -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> 'a
Sourceval replacing_dependency : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> 'a
Sourceval already_used : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval used_twice : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval variable_has_no_value : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval convert_incompatible_types : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'a
Sourceval convert_not_a_type : ?loc:Loc.t -> unit -> 'a
Sourceval not_convertible : ?loc:Loc.t -> unit -> 'a
Sourceval not_unfoldable : ?loc:Loc.t -> unit -> 'a
Sourceval no_quantified_hypothesis : ?loc:Loc.t -> Tactypes.quantified_hypothesis -> bool -> 'a
Sourceval cannot_find_instance : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval nothing_to_rewrite : ?loc:Loc.t -> Names.Id.t -> 'a
Sourceval ill_formed_elimination_type : ?loc:Loc.t -> unit -> 'a
Sourceval unable_to_apply_lemma : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'a
Sourceval depends_on_body : ?loc:Loc.t -> Names.Id.t list -> Names.Id.Set.t -> Names.Id.t option -> 'a
Sourceval not_right_number_constructors : ?loc:Loc.t -> int -> 'a
Sourceval not_enough_constructors : ?loc:Loc.t -> unit -> 'a
Sourceval constructors_numbered_from_one : ?loc:Loc.t -> unit -> 'a
Sourceval no_constructors : ?loc:Loc.t -> unit -> 'a
Sourceval unexpected_extra_pattern : ?loc:Loc.t -> int option -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr -> 'a
Sourceval cannot_find_inductive_argument : ?loc:Loc.t -> unit -> 'a
Sourceval one_intro_pattern_expected : ?loc:Loc.t -> unit -> 'a
Sourceval keep_and_clear_modifier_only_for_hypotheses : ?loc:Loc.t -> unit -> 'a
Sourceval fixpoint_on_non_inductive_type : ?loc:Loc.t -> unit -> 'a
Sourceval not_enough_products : ?loc:Loc.t -> unit -> 'a
Sourceval all_methods_in_coinductive_type : ?loc:Loc.t -> unit -> 'a
Sourceval replacement_ill_typed : ?loc:Loc.t -> exn -> 'a
Sourceval not_enough_premises : ?loc:Loc.t -> unit -> 'a
Sourceval need_dependent_product : ?loc:Loc.t -> unit -> 'a
Internal use only.
Sourceval clear_dependency_msg : Environ.env -> Evd.evar_map -> Names.Id.t option -> Evarutil.clear_dependency_error -> Names.GlobRef.t option -> Pp.t
Sourceexception NotConvertible
Sourceexception DependsOnBody of Names.Id.t list * Names.Id.Set.t * Names.Id.t option