From 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 5 Sep 2014 18:58:18 +0200
Subject: Retype terms resulting from the feeding of a context with a term.

Fixes bug #3455.
---
 tactics/tacinterp.ml | 9 ++++++---
 1 file 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",
-- 
cgit v1.2.3