diff options
Diffstat (limited to 'plugins/subtac/eterm.mli')
| -rw-r--r-- | plugins/subtac/eterm.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 413823ffe..1d1c51266 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -19,12 +19,12 @@ 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 * +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 *) |