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 +-
 test-suite/bugs/closed/bug_8755.v | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_8755.v

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
diff --git a/test-suite/bugs/closed/bug_8755.v b/test-suite/bugs/closed/bug_8755.v
new file mode 100644
index 0000000000..cd5aee4fa0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8755.v
@@ -0,0 +1,6 @@
+
+Lemma f : Type.
+Fail let i := ident:(i) in
+let t := context i [Type] in
+idtac.
+Abort.
-- 
cgit v1.2.3