diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 16:36:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:15:27 +0200 |
| commit | 666568377cbe1c18ce479d32f6359aa61af6d553 (patch) | |
| tree | 188217d9c0141ac95bab7bec24e021d13afc0084 /intf | |
| parent | c8986ad5589ad5bbed0936f9c16bba3f2ae1d2c4 (diff) | |
Type delayed_open_constr is now monotonic.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 45f482cd4..124d4c0fe 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,11 +122,12 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type delayed_open_constr_with_bindings = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } -type delayed_open_constr = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr +type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open + +type delayed_open_constr = Term.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr located type intro_patterns = delayed_open_constr intro_pattern_expr located list |