3 files changed, 19 insertions, 2 deletions
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
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 47741e439a..3b3351d330 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -46,3 +46,7 @@ match n with
 | plus2 _ :: _ => 2
 end
      : list(nat) -> nat
+# x : nat => x
+     : nat -> nat
+# _ : nat => 2
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e902a3c273..1fcbe858a8 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -83,3 +83,13 @@ Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 *)
+
+(* Check notations for functional terms which do not necessarily
+   depend on their parameter *)
+(* Old request mentioned again on coq-club 20/1/2012 *)
+
+Notation "#  x : T => t" := (fun x : T => t)
+  (at level 0, t at level 200, x ident).
+
+Check # x : nat => x.
+Check # _ : nat => 2.