diff options
| author | Pierre-Marie Pédrot | 2014-09-05 18:58:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-05 19:00:39 +0200 |
| commit | 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 (patch) | |
| tree | 72268d86220cce0703a3699a9ea105bb24b41661 | |
| parent | f1f8fa010bf0b9b645883306287fec41311971c5 (diff) | |
Retype terms resulting from the feeding of a context with a term.
Fixes bug #3455.
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 00ca189591..f4caefa705 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -671,9 +671,12 @@ let interp_may_eval f ist env sigma = function sigma , (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp) | ConstrContext ((loc,s),c) -> (try - let (sigma,ic) = f ist env sigma c - and ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in - sigma , subst_meta [ConstrMatching.special_meta,ic] ctxt + let (sigma,ic) = f ist env sigma c in + let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in + let evdref = ref sigma in + let c = subst_meta [ConstrMatching.special_meta,ic] ctxt in + let c = Typing.solve_evars env evdref c in + !evdref , c with | Not_found -> user_err_loc (loc, "interp_may_eval", |