Merge branch 'experimental/upstream' into upstream

1 files changed, 16 insertions, 0 deletions

diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
new file mode 100644
index 00000000..5c91292b
--- /dev/null
+++ b/plugins/funind/glob_term_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*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
+  Topconstr.constr_expr list -> (* The list of function returned type *)
+  Glob_term.glob_constr list -> (* the list of body *)
+  unit
+