From e343fb550c3cd452f0646782edd39c9b7a5a992b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 29 Aug 2014 08:58:40 +0200
Subject: Fixing commit 50237af2.

Indeed, generalized binders are unnamed, because their name is generated on the
fly.
---
 toplevel/command.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6d1ca685e..69c0aaea8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -463,7 +463,8 @@ let check_named (loc, na) = match na with
 
 let check_param = function
 | LocalRawDef (na, _) -> check_named na
-| LocalRawAssum (nas, _, _) -> List.iter check_named nas
+| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
+| LocalRawAssum (nas, Generalized _, _) -> ()
 
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
-- 
cgit v1.2.3