Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 19 insertions, 0 deletions

diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
new file mode 100644
index 00000000..ff98f2b9
--- /dev/null
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -0,0 +1,19 @@
+open Names
+open Term
+
+val prove_princ_for_struct :
+  bool ->
+  int -> constant array -> constr array -> int -> Tacmach.tactic
+
+
+val prove_principle_for_gen :
+  constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+  constr option ref -> (* a pointer to the obligation proofs lemma *)
+  bool -> (* is that function uses measure *)
+  int -> (* the number of recursive argument *)
+  types -> (* the type of the recursive argument *)
+  constr -> (* the wf relation used to prove the function *)
+  Tacmach.tactic
+
+
+(* val is_pte  : rel_declaration -> bool  *)