diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tactypes.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/intf/tactypes.mli b/intf/tactypes.mli index ef90b911c5..5c1d31946c 100644 --- a/intf/tactypes.mli +++ b/intf/tactypes.mli @@ -22,8 +22,7 @@ open Misctypes type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } +type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a type delayed_open_constr = EConstr.constr delayed_open type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open |