From 0bfa187edddb0de9bb75c55e1b3d0f08830c7ac8 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 5 Jun 2013 13:26:51 +0000
Subject: Replacing lists by maps in matching interpretation.

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

(limited to 'tactics/evar_tactics.ml')

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 87aff97fbe..e096ac4498 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Names
 open Errors
 open Evar_refiner
 open Tacmach
@@ -41,7 +42,9 @@ let instantiate n (ist,rawc) ido gl =
     if n <= 0 then error "Incorrect existential variable index.";
     let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
-    let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_filtered_env evi) in
+    let filtered = Evd.evar_filtered_env evi in
+    let (bvars, uvars) = Tacinterp.extract_ltac_constr_values ist filtered in
+    let ltac_vars = (Id.Map.bindings bvars, uvars) in
     let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
-- 
cgit v1.2.3