Index: src/Parser/parser.yy
===================================================================
--- src/Parser/parser.yy	(revision 94b1022a3fd279df5304e58231633a956e3fb672)
+++ src/Parser/parser.yy	(revision 863c413f24815aa1a75d3e6adbf647b31c863f8a)
@@ -10,6 +10,6 @@
 // Created On       : Sat Sep  1 20:22:55 2001
 // Last Modified By : Peter A. Buhr
-// Last Modified On : Wed May 30 20:29:03 2018
-// Update Count     : 3432
+// Last Modified On : Thu May 31 15:11:40 2018
+// Update Count     : 3444
 //
 
@@ -265,5 +265,5 @@
 %type<sn> statement						labeled_statement			compound_statement
 %type<sn> statement_decl				statement_decl_list			statement_list_nodecl
-%type<sn> selection_statement
+%type<sn> selection_statement			if_statement
 %type<sn> switch_clause_list_opt		switch_clause_list
 %type<en> case_value
@@ -404,26 +404,30 @@
 //************************* Namespace Management ********************************
 
-// The grammar in the ANSI C standard is not strictly context-free, since it relies upon the distinct terminal symbols
-// "identifier", "TYPEDEFname", and "TYPEGENname" that are lexically identical.  While it is possible to write a purely
-// context-free grammar, such a grammar would obscure the relationship between syntactic and semantic constructs.
-// Hence, this grammar uses the ANSI style.
-//
-// Cforall compounds this problem by introducing type names local to the scope of a declaration (for instance, those
-// introduced through "forall" qualifiers), and by introducing "type generators" -- parameterized types.  This latter
-// type name creates a third class of identifiers that must be distinguished by the scanner.
-//
-// Since the scanner cannot distinguish among the different classes of identifiers without some context information, it
-// accesses a data structure (TypedefTable) to allow classification of an identifier that it has just read.  Semantic
-// actions during the parser update this data structure when the class of identifiers change.
-//
-// Because the Cforall language is block-scoped, an identifier can change its class in a local scope; it must revert to
-// its original class at the end of the block.  Since type names can be local to a particular declaration, each
-// declaration is itself a scope.  This requires distinguishing between type names that are local to the current
-// declaration scope and those that persist past the end of the declaration (i.e., names defined in "typedef" or "otype"
-// declarations).
-//
-// The non-terminals "push" and "pop" denote the opening and closing of scopes.  Every push must have a matching pop,
-// although it is regrettable the matching pairs do not always occur within the same rule.  These non-terminals may
-// appear in more contexts than strictly necessary from a semantic point of view.
+// The C grammar is not context free because it relies on the distinct terminal symbols "identifier" and "TYPEDEFname",
+// which are lexically identical.
+//
+//   typedef int foo; // identifier foo must now be scanned as TYPEDEFname
+//   foo f;           // to allow it to appear in this context
+//
+// While it may be possible to write a purely context-free grammar, such a grammar would obscure the relationship
+// between syntactic and semantic constructs.  Cforall compounds this problem by introducing type names local to the
+// scope of a declaration (for instance, those introduced through "forall" qualifiers), and by introducing "type
+// generators" -- parameterized types.  This latter type name creates a third class of identifiers, "TYPEGENname", which
+// must be distinguished by the lexical scanner.
+//
+// Since the scanner cannot distinguish among the different classes of identifiers without some context information,
+// there is a type table (typedefTable), which holds type names and identifiers that override type names, for each named
+// scope. During parsing, semantic actions update the type table by adding new identifiers in the current scope. For
+// each context that introduces a name scope, a new level is created in the type table and that level is popped on
+// exiting the scope.  Since type names can be local to a particular declaration, each declaration is itself a scope.
+// This requires distinguishing between type names that are local to the current declaration scope and those that
+// persist past the end of the declaration (i.e., names defined in "typedef" or "otype" declarations).
+//
+// The non-terminals "push" and "pop" denote the opening and closing of named scopes. Every push has a matching pop in
+// the production rule. There are multiple lists of declarations, where each declaration is a named scope, so pop/push
+// around the list separator.
+//
+//  int f( forall(T) T (*f1) T , forall( S ) S (*f2)( S ) );
+//      push               pop   push                   pop
 
 push:
@@ -952,9 +956,8 @@
 
 selection_statement:
-	IF '(' push if_control_expression ')' statement pop		%prec THEN
-		// explicitly deal with the shift/reduce conflict on if/else
-		{ $$ = new StatementNode( build_if( $4, $6, nullptr ) ); }
-	| IF '(' push if_control_expression ')' statement ELSE statement pop
-		{ $$ = new StatementNode( build_if( $4, $6, $8 ) ); }
+			// pop causes a S/R conflict without separating the IF statement into a non-terminal even after resolving
+			// the inherent S/R conflict with THEN/ELSE.
+	push if_statement pop
+		{ $$ = $2; }
 	| SWITCH '(' comma_expression ')' case_clause
 		{ $$ = new StatementNode( build_switch( true, $3, $5 ) ); }
@@ -977,4 +980,13 @@
 		}
 	;
+
+if_statement:
+	IF '(' if_control_expression ')' statement			%prec THEN
+		// explicitly deal with the shift/reduce conflict on if/else
+		{ $$ = new StatementNode( build_if( $3, $5, nullptr ) ); }
+	| IF '(' if_control_expression ')' statement ELSE statement
+		{ $$ = new StatementNode( build_if( $3, $5, $7 ) ); }
+	;
+
 
 if_control_expression:
@@ -1172,8 +1184,8 @@
 
 handler_clause:
-	handler_key '(' push push exception_declaration pop handler_predicate_opt ')' compound_statement pop
-		{ $$ = new StatementNode( build_catch( $1, $5, $7, $9 ) ); }
-	| handler_clause handler_key '(' push push exception_declaration pop handler_predicate_opt ')' compound_statement pop
-		{ $$ = (StatementNode *)$1->set_last( new StatementNode( build_catch( $2, $6, $8, $10 ) ) ); }
+	handler_key '(' push exception_declaration pop handler_predicate_opt ')' compound_statement pop
+		{ $$ = new StatementNode( build_catch( $1, $4, $6, $8 ) ); }
+	| handler_clause handler_key '(' push exception_declaration pop handler_predicate_opt ')' compound_statement pop
+		{ $$ = (StatementNode *)$1->set_last( new StatementNode( build_catch( $2, $5, $7, $9 ) ) ); }
 	;
 
