From ecead0d68bc8b1359617e274a7aa8d8bee3aeb77 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Jun 2004 10:24:24 +0000
Subject: Ajout de la coercion id dans context vers evaluable constant (bug
 #777)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5841 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fe557c9fcf..3c2e05f0a3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -219,6 +219,8 @@ let coerce_to_evaluable_ref env c =
   let ev = match c with
     | VConstr c when isConst c -> EvalConstRef (destConst c)
     | VConstr c when isVar c -> EvalVarRef (destVar c)
+    | VIntroPattern (IntroIdentifier id)
+	when Environ.evaluable_named id env -> EvalVarRef id
     | _ -> error_not_evaluable (pr_value env c)
   in
   if not (Tacred.is_evaluable env ev) then
-- 
cgit v1.2.3