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

1 files changed, 31 insertions, 0 deletions

diff --git a/contrib/funind/functional_principles_types.mli b/contrib/funind/functional_principles_types.mli
new file mode 100644
index 00000000..8b4faaf4
--- /dev/null
+++ b/contrib/funind/functional_principles_types.mli
@@ -0,0 +1,31 @@
+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 : (identifier*identifier*Rawterm.rawsort) list ->  unit
+val make_case_scheme : (identifier*identifier*Rawterm.rawsort)  ->  unit