The contribution of Pierre Courtieu on generating specialized induction schemes

for recursive functions.


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

1 files changed, 75 insertions, 0 deletions

diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
new file mode 100644
index 000000000..21e351371
--- /dev/null
+++ b/contrib/funind/tacinvutils.mli
@@ -0,0 +1,75 @@
+(* tacinvutils.ml *)
+(*s utilities *)
+
+(*i*)
+open Termops
+open Equality
+open Names
+open Pp
+open Tacmach
+open Proof_type
+open Tacinterp
+open Tactics
+open Tacticals
+open Term
+open Util
+open Printer
+open Reductionops
+open Inductiveops
+open Coqlib
+open Refine
+open Evd
+(*i*)
+
+(* printing *)
+val prconstr: constr -> unit
+val prlistconstr: constr list  -> unit
+val prstr: string -> unit 
+
+
+val mknewmeta: unit -> constr
+val mknewexist: unit -> existential
+val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
+val mkEq: types -> constr -> constr -> constr
+(* let mkEq typ c1 c2 =   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
+val mkRefl: types -> constr -> constr
+val buildrefl_from_eqs: constr list -> constr list
+(* typ c1 =  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), [| typ; c1|]) *)
+
+val nth_dep_constructor: constr -> int -> (constr*int)
+
+val prod_it_lift:  (name*constr) list -> constr -> constr
+val prod_it_anonym_lift: constr -> constr list -> constr
+val lam_it_anonymous: constr -> constr list -> constr
+val lift1L: (constr list) -> constr list
+val popn: int -> constr -> constr
+val lambda_id: constr -> constr -> constr -> constr
+val prod_id: constr -> constr -> constr -> constr
+
+
+val name_of_string : string -> name
+val newname_append: name -> string -> name
+
+val apply_eqtrpl: (constr*constr*constr) -> constr -> constr
+val substitterm: int -> constr -> constr -> constr -> constr
+val apply_leqtrpl_t: 
+  constr -> (constr*constr*constr) list -> constr
+val apply_eq_leqtrpl: 
+  (constr*constr*constr) list -> constr -> (constr*constr*constr) list
+(* val apply_leq_lt: constr list -> constr list -> constr list *)
+
+val hdMatchSub: constr -> constr -> constr list
+val hdMatchSub_cpl: constr -> int*int -> constr list
+val exchange_hd_prod: constr -> constr -> constr
+val exchange_reli_arrayi_L: constr array  -> int*int -> constr list -> constr list
+val substit_red: int -> constr -> constr -> constr -> constr
+val expand_letins: constr -> constr
+
+val def_of_const: constr -> constr
+val name_of_const: constr -> string
+(*i
+ Local Variables:
+ compile-command: "make -k tacinvutils.cmi"
+ End:
+i*)
+