From 22a8453f551349bbafa14b914aa784693dcf3615 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 21:08:33 +0000
Subject: Notations with binders: Accepting using notations for functional
 terms which do not necessarily depend on their parameter (e.g. a notation for
 "fun x => t" might match also "fun _ => t").

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

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0db70e59c1..32f20e0a84 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -564,8 +564,11 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | _ -> raise No_match
 
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 (fst metas) ->
-      alp, bind_env alp sigma id2 (GVar (dummy_loc,id1))
+  | (_,Name id2) when List.mem id2 (fst metas) ->
+      let rhs = match na1 with
+      | Name id1 -> GVar (dummy_loc,id1)
+      | Anonymous -> GHole (dummy_loc,Evd.InternalHole) in
+      alp, bind_env alp sigma id2 rhs
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
-- 
cgit v1.2.3