diff options
Diffstat (limited to 'plugins/funind/gen_principle.mli')
| -rw-r--r-- | plugins/funind/gen_principle.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli index 06ece6feee..7eb8ca3af1 100644 --- a/plugins/funind/gen_principle.mli +++ b/plugins/funind/gen_principle.mli @@ -15,3 +15,9 @@ val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas. val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit val make_graph : Names.GlobRef.t -> unit + +(* Can be thrown by build_{,case}_scheme *) +exception No_graph_found + +val build_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) list -> unit +val build_case_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) -> unit |