diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 09:57:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 10:05:03 +0200 |
| commit | 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 (patch) | |
| tree | 7747e567b36ce6db92154eaeedbe95eaa723c751 /tactics | |
| parent | d30a7244b52e86c364320a8fa0794c7686f30074 (diff) | |
Backtracking on interpreting toplevel calls to exact in scope determined
by the type to prove (was introduced in 35846ec22, r15978, Nov 2012).
Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.
Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...
See #4034 for a discussion.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5a0d26a1c..6c125ed2d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -557,7 +557,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; } in - intern_gen kind ~allow_patvar ~ltacvars env c + let kind_for_intern = + match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in + intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in |