Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7

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 000000000..62eb528e0
--- /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  *)