From 97f3bb671ba3123e944de38a3cab131946103185 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 17 Dec 2012 17:53:20 +0000
Subject: Fixed interpretation of "x" as a binding variable for the return
 predicate in "match x return ... with" when x is a goal variable. Commit 4926
 forbade it but too strongly. AFAICS, only notation variables have to be
 avoided.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16083 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4fff70db7..8d44bc5317 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1504,7 +1504,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | GVar (loc,id), None when Id.Set.mem id env.ids -> Some id,(loc,Name id)
+      | GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) -> Some id,(loc,Name id)
       | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
-- 
cgit v1.2.3