diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /plugins/ltac/tacexpr.mli | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
Diffstat (limited to 'plugins/ltac/tacexpr.mli')
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index b78dc37426..cfb698cd87 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -117,8 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = 'a Tactypes.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_with_bindings = EConstr.constr with_bindings delayed_open |