diff options
| author | Hugo Herbelin | 2014-08-15 17:43:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:39 +0200 |
| commit | 5dcafa956e49eefc451dd021a0fe8ad2e2338088 (patch) | |
| tree | c851c0f1cb32815bae652309c39f6d4a681fd2cc /intf | |
| parent | 72498d6d68ac12ba4db0db7d54f0ac6fdaaf0c61 (diff) | |
Lazy interpretation of patterns so that expressions such as "intros H H'/H"
can be given with second H bound by the first one.
Not very satisfied by passing closure to tactics.ml, but otherwise
tactics would have to be aware of glob_constr.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 9b75282ca1..abb2292cd1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -106,9 +106,16 @@ type open_glob_constr = unit * glob_constr_and_expr type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type intro_pattern = Term.constr intro_pattern_expr located -type intro_patterns = Term.constr intro_pattern_expr located list -type or_and_intro_pattern = Term.constr or_and_intro_pattern_expr located +type delayed_open_constr_with_bindings = + Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings + +type delayed_open_constr = + Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr + +type intro_pattern = delayed_open_constr intro_pattern_expr located +type intro_patterns = delayed_open_constr intro_pattern_expr located list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located +type intro_pattern_naming = intro_pattern_naming_expr located (** Generic expressions for atomic tactics *) |