1 files changed, 0 insertions, 80 deletions
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
deleted file mode 100644
index 64b21213..00000000
--- a/contrib/funind/tacinvutils.mli
+++ /dev/null
@@ -1,80 +0,0 @@
-(* 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 debugging *)
-val prconstr: constr -> unit
-val prlistconstr: constr list  -> unit
-val prNamedConstr:string -> constr -> unit
-val prNamedLConstr:string -> constr list -> unit
-val prstr: string -> unit 
-
-
-val mknewmeta: unit -> constr
-val mknewexist: unit -> existential
-val resetmeta: unit -> unit (* safe *)
-val resetexist: unit -> unit (* be careful with this one *)
-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 -> constr
-val substitterm: int -> constr -> constr -> constr -> constr
-val apply_leqtrpl_t: 
-  constr -> (constr*(constr*constr*constr)) list -> constr
-val apply_eq_leqtrpl: 
-  (constr*(constr*constr*constr)) list -> constr -> (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 -C ../.. contrib/funind/tacinvutils.cmi" ***
- *** End: ***
-i*)
-