Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 16 insertions, 0 deletions

diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/rawterm_to_relation.mli
new file mode 100644
index 00000000..a314050f
--- /dev/null
+++ b/plugins/funind/rawterm_to_relation.mli
@@ -0,0 +1,16 @@
+
+
+
+(*
+  [build_inductive parametrize funnames funargs returned_types bodies]
+  constructs and saves the graphs of the functions [funnames] taking [funargs] as arguments
+  and returning [returned_types] using bodies [bodies]
+*)
+
+val build_inductive :
+  Names.identifier list -> (* The list of function name *)
+  (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
+  Topconstr.constr_expr list -> (* The list of function returned type *)
+  Rawterm.rawconstr list -> (* the list of body *)
+  unit
+