diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/subtac/eterm.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/subtac/eterm.mli')
| -rw-r--r-- | contrib/subtac/eterm.mli | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli deleted file mode 100644 index 19e8ffe8..00000000 --- a/contrib/subtac/eterm.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: eterm.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) -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_defs -> evar_map -> int -> - ?status:obligation_definition_status -> constr -> types -> - (identifier * types * loc * obligation_definition_status * Intset.t * - Tacexpr.raw_tactic_expr option) array * constr * types - (* Obl. name, type as product, location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - -val etermtac : open_constr -> tactic |