From 6d5425d3f0ac6a0d78d51ba566d46e1bd50f5a20 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Dec 2002 10:26:29 +0000
Subject: Protection contre les variables anonymes dans match_aconstr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3413 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1be41458d4..7c1e9aea5e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -232,7 +232,13 @@ type interpretation = (identifier * scope_name list) list * aconstr
 let match_aconstr c (metas_scl,pat) =
   let subst = match_ [] (List.map fst metas_scl) [] c pat in
   (* Reorder canonically the substitution *)
-  List.map (fun (x,scl) -> (List.assoc x subst,scl)) metas_scl
+  let find x subst =
+    try List.assoc x subst
+    with Not_found ->
+      (* Happens for binders bound to Anonymous *)
+      (* Find a better way to propagate Anonymous... *)
+      RVar (dummy_loc,x) in
+  List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
-- 
cgit v1.2.3