Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 33 deletions

diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
deleted file mode 100644
index 35744b71..00000000
--- a/plugins/subtac/eterm.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Environ
-open Tacmach
-open Term
-open Evd
-open Names
-open Util
-open Tacinterp
-
-val mkMetas : int -> constr list
-
-val evar_dependencies : evar_map -> int -> Intset.t
-val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
-
-(* env, id, evars, number of function prototypes to try to clear from
-   evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
-  ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * hole_kind located * obligation_definition_status * Intset.t * 
-      tactic option) array
-    (* Existential key, obl. name, type as product, location of the original evar, associated tactic,
-       status and dependencies as indexes into the array *)
-  * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types
-    (* Translations from existential identifiers to obligation identifiers 
-       and for terms with existentials to closed terms, given a 
-       translation from obligation identifiers to constrs, new term, new type *)