diff options
Diffstat (limited to 'contrib/subtac/eterm.mli')
| -rw-r--r-- | contrib/subtac/eterm.mli | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index bf854abb3..e197024ff 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -16,11 +16,12 @@ open Util val mkMetas : int -> constr 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 +(* 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) array * constr * types (* Obl. name, type as product, location of the original evar, - opacity (true = opaque) and dependencies as indexes into the array *) + status and dependencies as indexes into the array *) val etermtac : open_constr -> tactic |