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, 34 insertions, 0 deletions

diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
new file mode 100644
index 000000000..cf28c6e6c
--- /dev/null
+++ b/plugins/funind/functional_principles_types.mli
@@ -0,0 +1,34 @@
+open Names
+open Term
+
+
+val generate_functional_principle : 
+  (* do we accept interactive proving *)
+  bool ->
+  (* induction principle on rel *) 
+  types ->
+  (* *)
+  sorts array option -> 
+  (* Name of the new principle *) 
+  (identifier) option -> 
+  (* the compute functions to use   *)
+  constant array -> 
+  (* We prove the nth- principle *)
+  int  ->
+  (* The tactic to use to make the proof w.r
+     the number of params
+  *)
+  (constr array -> int -> Tacmach.tactic) -> 
+  unit
+
+val compute_new_princ_type_from_rel : constr array -> sorts array -> 
+  types -> types
+
+
+exception No_graph_found
+
+val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
+
+val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list ->  unit
+val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort)  ->  unit
+