From 8e88b7adab785146815e2fb25faf9b11fab989e8 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 1 Aug 2013 17:22:44 +0000
Subject: Fixing #3088. Translation from globconstrs to patterns was forgetting
 to register bound variables as such in the return clause.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16649 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/patternops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d695e8a45e..3623828f42 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -360,7 +360,8 @@ let rec pat_of_raw metas vars = function
       in
       let pred = match p,indnames with
 	| Some p, Some (_,_,nal) ->
-	  rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p))
+          let nvars = List.rev_append nal (na :: vars) in
+          rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
 	| _ -> PMeta None
       in
       let info =
-- 
cgit v1.2.3