From 1c5f5f658c95def5cf19fdf5fdb2fe0a0aa1c740 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 24 Jun 2013 12:56:39 +0000
Subject: Using the whole tactic environment while Pretyping.

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

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b32e6731ee..7470de6c93 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -406,15 +406,7 @@ let extract_ltac_constr_values ist env =
       let c = coerce_to_constr env v in
       (Id.Map.add id c vars1, vars2)
     with CannotCoerceTo _ ->
-      let ido =
-        let v = Value.normalize v in
-        if has_type v (topwit wit_intro_pattern) then
-          match out_gen (topwit wit_intro_pattern) v with
-          | _, IntroIdentifier id0 -> Some id0
-          | _ -> None
-        else None
-      in
-      (vars1, Id.Map.add id ido vars2)
+      (vars1, Id.Map.add id v vars2)
   in
   Id.Map.fold fold ist.lfun (Id.Map.empty, Id.Map.empty)
 (** ppedrot: I have changed the semantics here. Before this patch, closure was
-- 
cgit v1.2.3