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 /tactics/tacinterp.ml | |
| 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 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 026ed94a4c..df31152659 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -725,7 +725,9 @@ let rec message_of_value env v = else if has_type v (topwit wit_unit) then str "()" else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v) else if has_type v (topwit wit_intro_pattern) then - Miscprint.pr_intro_pattern (pr_constr_env env) (out_gen (topwit wit_intro_pattern) v) + Miscprint.pr_intro_pattern + (fun c -> pr_constr_env env (snd (c env Evd.empty))) + (out_gen (topwit wit_intro_pattern) v) else if has_type v (topwit wit_constr_context) then pr_constr_env env (out_gen (topwit wit_constr_context) v) else match Value.to_list v with @@ -776,7 +778,7 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn (c,ipat) -> - let sigma,c = interp_constr ist env sigma c in + let c = fun env sigma -> interp_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn (c,ipat) | IntroRewrite _ as x -> sigma, x |