diff options
Diffstat (limited to 'contrib/subtac/eterm.mli')
| -rw-r--r-- | contrib/subtac/eterm.mli | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 007e327c..19e8ffe8 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,23 +6,27 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 10889 2008-05-06 14:05:20Z msozeau $ i*) +(*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 eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) 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 -> constr -> types -> - (identifier * types * loc * bool * Intset.t) array * constr * types - (* Obl. name, type as product, location of the original evar, - opacity (true = opaque) and dependencies as indexes into the array *) +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 |