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".

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa620c1d..ef454299e 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