From d68f695b5a953c50bcf5e80182ef317682de1a05 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Jul 2019 14:01:38 +0200
Subject: [vernacexpr] Refactor fixpoint AST.

We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.

More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.

Feedback on the naming of the records fields is welcome.

This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.

cc: #6019
---
 plugins/funind/indfun.mli | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'plugins/funind/indfun.mli')

diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 3bc52272ac..bfc9686ae5 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,12 +5,9 @@ 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 :
-  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
+val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
 
-val do_generate_principle_interactive :
-  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Lemmas.t
+val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t
 
 val functional_induction :
   bool ->
-- 
cgit v1.2.3