added mli 's for the nex functional induction (forgotten last time).

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

1 files changed, 39 insertions, 0 deletions

diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
new file mode 100644
index 000000000..639063faf
--- /dev/null
+++ b/contrib/funind/indfun_common.mli
@@ -0,0 +1,39 @@
+open Names
+open Pp
+
+val mk_rel_id : identifier -> identifier
+
+val msgnl : std_ppcmds -> unit
+
+val invalid_argument : string -> 'a
+
+val fresh_id : identifier list -> string -> identifier
+val fresh_name : identifier list -> string -> name 
+val get_name : identifier list -> ?default:string -> name -> name 
+
+val array_get_start : 'a array -> 'a array
+
+val id_of_name : name -> identifier
+
+val locate_ind : Libnames.reference -> inductive
+val locate_constant : Libnames.reference -> constant
+val locate_with_msg :
+  Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
+  Libnames.reference -> 'a
+
+val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
+val list_union_eq :
+  ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
+val list_add_set_eq :
+  ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+
+val chop_rlambda_n : int -> Rawterm.rawconstr ->
+  (name*Rawterm.rawconstr) list * Rawterm.rawconstr
+
+val chop_rprod_n : int -> Rawterm.rawconstr ->
+  (name*Rawterm.rawconstr) list * Rawterm.rawconstr
+
+val def_of_const : Term.constr -> Term.constr
+val eq : Term.constr Lazy.t
+val refl_equal : Term.constr Lazy.t
+val const_of_id: identifier -> constant