From b1656b1f10501b34ae6a7e147f550710b935e54b Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Wed, 22 Mar 2017 20:35:38 -0400
Subject: Intern names bound in match patterns

Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
---
 pretyping/patternops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fe73b6105b..2090aad8a0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -404,7 +404,9 @@ let rec pat_of_raw metas vars = function
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
-    | PatVar(_,na) -> na
+    | PatVar(_,na) ->
+      name_iter (fun n -> metas := n::!metas) na;
+      na
     | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
-- 
cgit v1.2.3