diff options
Diffstat (limited to 'plugins/funind/gen_principle.mli')
| -rw-r--r-- | plugins/funind/gen_principle.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli index 3c04d6cb7d..28751c4501 100644 --- a/plugins/funind/gen_principle.mli +++ b/plugins/funind/gen_principle.mli @@ -12,7 +12,7 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle_interactive : - Vernacexpr.fixpoint_expr list -> Lemmas.t + Vernacexpr.fixpoint_expr list -> Declare.Proof.t val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit val make_graph : Names.GlobRef.t -> unit |