From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 02:18:53 +0100
Subject: A fix to #5414 (ident bound by ltac names now known for "match").

Also taking into account a name in the return clause and in the
indices.

Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
---
 proofs/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa620c1da..ef454299ea 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -428,7 +428,7 @@ module V82 = struct
       in
       let env = Evd.evar_filtered_env evi in
       let rawc = Constrintern.intern_constr env com in
-      let ltac_vars = Pretyping.empty_lvar in
+      let ltac_vars = Glob_ops.empty_lvar in
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-- 
cgit v1.2.3