From 34ba48a885c91ea895cbba7ba5a53b1ec9de5db8 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 13 Feb 2007 18:47:49 +0000
Subject: Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
 fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn")
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'pretyping/pattern.ml')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 979ecb0b1..b0fd76cb7 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -216,7 +216,7 @@ let rec pat_of_raw metas vars = function
       PRef r
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
   | RApp (_, RPatVar (_,(true,n)), cl) ->
-      PSoApp (n, List.map (pat_of_raw metas vars) cl)
+      metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
   | RApp (_,c,cl) -> 
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-- 
cgit v1.2.3