Fixing bug #1944 ("assert false" with ? in nested intro patterns).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.1@11791 85f007b7-540e-0410-9357-904b9bb8a0f7
coq · Jan 15, 2009 · 951cd9b · 951cd9b
1 parent e8a5f43
commit 951cd9b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
@@ -1220,7 +1220,7 @@ let rec first_name_buggy = function
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
-  | IntroAnonymous -> assert false
+  | IntroAnonymous -> (* buggy *) None
 
 let consume_pattern avoid id gl = function
   | [] -> (IntroIdentifier (fresh_id avoid id gl), [])