Suppression capture des variables par lieurs non liés dans Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6313 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 2 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 28f0de932..35162a563 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -718,8 +718,14 @@ let coerce_to_id = function
         str"This expression should be a simple identifier")
 
 let traverse_binder subst id (ids,tmpsc,scopes as env) =
-  let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
-  id,(Idset.add id ids,tmpsc,scopes)
+  try
+    (* Binders bound in the notation are consider first-order object *)
+    (* and binders not bound in the notation do not capture variables *)
+    (* outside the notation *)
+    let id' = coerce_to_id (fst (List.assoc id subst)) in
+    id', (Idset.add id' ids,tmpsc,scopes)
+  with Not_found ->
+    id, env
 
 let decode_constrlist_value = function
   | CAppExpl (_,_,l) -> l