Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 20 insertions, 0 deletions

diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
new file mode 100644
index 00000000..35da5d50
--- /dev/null
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -0,0 +1,20 @@
+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 
+val do_observe : unit -> bool