From 09122b77b4f556281fec338cbb2ec43c5520dc8d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Nov 2017 18:03:11 +0100
Subject: Again one more step in fixing #5762 ("where" clause).

We enforce that variables of the notation hide the variables in the
implicit-arguments map.

Will be useful when there will be a special map of single binders
when interpreting notations.
---
 interp/constrintern.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4afe301dd7..b52a280291 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2161,6 +2161,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
 let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
+  let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
   let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
 						tmp_scope = None; scopes = []; impls = impls}
     false (empty_ltac_sign, vl) a in
-- 
cgit v1.2.3