From 0cad7b36e43bcafd999d8266573be30387fd32d4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 18 Oct 2018 11:41:44 +0200
Subject: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.

---
 plugins/ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f90e889678..647d539127 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -687,7 +687,7 @@ let interp_may_eval f ist env sigma = function
   | ConstrContext ({loc;v=s},c) ->
       (try
 	let (sigma,ic) = f ist env sigma c in
-	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+        let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in
 	let ctxt = EConstr.Unsafe.to_constr ctxt in
         let ic = EConstr.Unsafe.to_constr ic in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-- 
cgit v1.2.3