Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 843054c23fcb725d2486e5e42e91b3741bc523b8)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 0f19d763a07f96324b450e9bafd7fdd52807ea0f)
@@ -89,4 +89,5 @@
 		};
 
+		/// Prunes a list of alternatives down to those that have the minimum conversion cost for a given return type; skips ambiguous interpretations
 		template< typename InputIterator, typename OutputIterator >
 		void pruneAlternatives( InputIterator begin, InputIterator end, OutputIterator out, const SymTab::Indexer &indexer ) {
@@ -108,10 +109,10 @@
 							std::cout << "cost " << candidate->cost << " beats " << mapPlace->second.candidate->cost << std::endl;
 							)
-							selected[ mangleName ] = current;
+						selected[ mangleName ] = current;
 					} else if ( candidate->cost == mapPlace->second.candidate->cost ) {
 						PRINT(
 							std::cout << "marking ambiguous" << std::endl;
 							)
-							mapPlace->second.isAmbiguous = true;
+						mapPlace->second.isAmbiguous = true;
 					}
 				} else {
@@ -124,14 +125,14 @@
 				)
 
-				// accept the alternatives that were unambiguous
-				for ( std::map< std::string, PruneStruct >::iterator target = selected.begin(); target != selected.end(); ++target ) {
-					if ( ! target->second.isAmbiguous ) {
-						Alternative &alt = *target->second.candidate;
-						for ( std::list< Type* >::iterator result = alt.expr->get_results().begin(); result != alt.expr->get_results().end(); ++result ) {
-							alt.env.applyFree( *result );
-						}
-						*out++ = alt;
+			// accept the alternatives that were unambiguous
+			for ( std::map< std::string, PruneStruct >::iterator target = selected.begin(); target != selected.end(); ++target ) {
+				if ( ! target->second.isAmbiguous ) {
+					Alternative &alt = *target->second.candidate;
+					for ( std::list< Type* >::iterator result = alt.expr->get_results().begin(); result != alt.expr->get_results().end(); ++result ) {
+						alt.env.applyFree( *result );
 					}
+					*out++ = alt;
 				}
+			}
 
 		}
@@ -184,5 +185,5 @@
 				printAlts( finder.alternatives, std::cout );
 				)
-				*out++ = finder;
+			*out++ = finder;
 		}
 	}
@@ -206,5 +207,5 @@
 			printAlts( alternatives, std::cout );
 			)
-			AltList::iterator oldBegin = alternatives.begin();
+		AltList::iterator oldBegin = alternatives.begin();
 		pruneAlternatives( alternatives.begin(), alternatives.end(), front_inserter( alternatives ), indexer );
 		if ( alternatives.begin() == oldBegin ) {
@@ -222,5 +223,5 @@
 			std::cout << "there are " << alternatives.size() << " alternatives after elimination" << std::endl;
 			)
-			}
+	}
 
 	void AlternativeFinder::findWithAdjustment( Expression *expr ) {
@@ -353,5 +354,4 @@
 
 	bool AlternativeFinder::instantiateFunction( std::list< DeclarationWithType* >& formals, /*const*/ AltList &actuals, bool isVarArgs, OpenVarSet& openVars, TypeEnvironment &resultEnv, AssertionSet &resultNeed, AssertionSet &resultHave ) {
-		std::list< TypeEnvironment > toBeDone;
 		simpleCombineEnvironments( actuals.begin(), actuals.end(), resultEnv );
 		// make sure we don't widen any existing bindings
@@ -382,7 +382,7 @@
 					std::cerr << std::endl;
 					)
-					if ( ! unify( (*formal)->get_type(), *actual, resultEnv, resultNeed, resultHave, openVars, indexer ) ) {
-						return false;
-					}
+				if ( ! unify( (*formal)->get_type(), *actual, resultEnv, resultNeed, resultHave, openVars, indexer ) ) {
+					return false;
+				}
 				formal++;
 			}
@@ -430,5 +430,5 @@
 					printAssertionSet( newNeed, std::cerr, 8 );
 					)
-					inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
+				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
 				return;
 			}
@@ -445,5 +445,5 @@
 			std::cerr << std::endl;
 			)
-			std::list< DeclarationWithType* > candidates;
+		std::list< DeclarationWithType* > candidates;
 		decls.lookupId( curDecl->get_name(), candidates );
 ///   if ( candidates.empty() ) { std::cout << "no candidates!" << std::endl; }
@@ -454,5 +454,5 @@
 				std::cout << std::endl;
 				)
-				AssertionSet newHave, newerNeed( newNeed );
+			AssertionSet newHave, newerNeed( newNeed );
 			TypeEnvironment newEnv( newAlt.env );
 			OpenVarSet newOpenVars( openVars );
@@ -467,31 +467,31 @@
 				std::cerr << std::endl;
 				)
-				if ( unify( curDecl->get_type(), adjType, newEnv, newerNeed, newHave, newOpenVars, indexer ) ) {
-					PRINT(
-						std::cerr << "success!" << std::endl;
-						)
-						SymTab::Indexer newDecls( decls );
-					addToIndexer( newHave, newDecls );
-					Alternative newerAlt( newAlt );
-					newerAlt.env = newEnv;
-					assert( (*candidate)->get_uniqueId() );
-					Expression *varExpr = new VariableExpr( static_cast< DeclarationWithType* >( Declaration::declFromId( (*candidate)->get_uniqueId() ) ) );
-					deleteAll( varExpr->get_results() );
-					varExpr->get_results().clear();
-					varExpr->get_results().push_front( adjType->clone() );
-					PRINT(
-						std::cout << "satisfying assertion " << curDecl->get_uniqueId() << " ";
-						curDecl->print( std::cout );
-						std::cout << " with declaration " << (*candidate)->get_uniqueId() << " ";
-						(*candidate)->print( std::cout );
-						std::cout << std::endl;
-						)
-						ApplicationExpr *appExpr = static_cast< ApplicationExpr* >( newerAlt.expr );
-					// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
-					appExpr->get_inferParams()[ curDecl->get_uniqueId() ] = ParamEntry( (*candidate)->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
-					inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, level, indexer, out );
-				} else {
-					delete adjType;
-				}
+			if ( unify( curDecl->get_type(), adjType, newEnv, newerNeed, newHave, newOpenVars, indexer ) ) {
+				PRINT(
+					std::cerr << "success!" << std::endl;
+					)
+				SymTab::Indexer newDecls( decls );
+				addToIndexer( newHave, newDecls );
+				Alternative newerAlt( newAlt );
+				newerAlt.env = newEnv;
+				assert( (*candidate)->get_uniqueId() );
+				Expression *varExpr = new VariableExpr( static_cast< DeclarationWithType* >( Declaration::declFromId( (*candidate)->get_uniqueId() ) ) );
+				deleteAll( varExpr->get_results() );
+				varExpr->get_results().clear();
+				varExpr->get_results().push_front( adjType->clone() );
+				PRINT(
+					std::cout << "satisfying assertion " << curDecl->get_uniqueId() << " ";
+					curDecl->print( std::cout );
+					std::cout << " with declaration " << (*candidate)->get_uniqueId() << " ";
+					(*candidate)->print( std::cout );
+					std::cout << std::endl;
+					)
+				ApplicationExpr *appExpr = static_cast< ApplicationExpr* >( newerAlt.expr );
+				// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
+				appExpr->get_inferParams()[ curDecl->get_uniqueId() ] = ParamEntry( (*candidate)->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
+				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, level, indexer, out );
+			} else {
+				delete adjType;
+			}
 		}
 	}
@@ -510,5 +510,5 @@
 			decls.print( std::cout );
 			)
-			addToIndexer( have, decls );
+		addToIndexer( have, decls );
 		AssertionSet newNeed;
 		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
@@ -534,5 +534,5 @@
 				printAssertionSet( resultNeed, std::cout, 8 );
 				)
-				inferParameters( resultNeed, resultHave, newAlt, openVars, out );
+			inferParameters( resultNeed, resultHave, newAlt, openVars, out );
 		}
 	}
@@ -542,5 +542,7 @@
 		AlternativeFinder funcOpFinder( indexer, env );
 
-		AlternativeFinder funcFinder( indexer, env ); {
+		AlternativeFinder funcFinder( indexer, env );
+
+		{
 			NameExpr *fname;
 			if ( ( fname = dynamic_cast<NameExpr *>( untypedExpr->get_function()))
@@ -560,5 +562,5 @@
 		Tuples::TupleAssignSpotter tassign( this );
 		if ( tassign.isTupleAssignment( untypedExpr, possibilities ) ) {
-			// take care of possible tuple assignments, or discard expression
+			// TODO take care of possible tuple assignments, or discard expression
 			return;
 		} // else ...
@@ -571,6 +573,6 @@
 				func->print( std::cout, 8 );
 				)
-				// check if the type is pointer to function
-				PointerType *pointer;
+			// check if the type is pointer to function
+			PointerType *pointer;
 			if ( func->expr->get_results().size() == 1 && ( pointer = dynamic_cast< PointerType* >( func->expr->get_results().front() ) ) ) {
 				if ( FunctionType *function = dynamic_cast< FunctionType* >( pointer->get_base() ) ) {
@@ -604,5 +606,5 @@
 						printAlts( funcOpFinder.alternatives, std::cout, 8 );
 						)
-						}
+				}
 
 				for ( AltList::const_iterator funcOp = funcOpFinder.alternatives.begin(); funcOp != funcOpFinder.alternatives.end(); ++funcOp ) {
@@ -737,22 +739,22 @@
 		indexer.lookupId( nameExpr->get_name(), declList );
 		PRINT( std::cerr << "nameExpr is " << nameExpr->get_name() << std::endl; )
-			for ( std::list< DeclarationWithType* >::iterator i = declList.begin(); i != declList.end(); ++i ) {
-				VariableExpr newExpr( *i, nameExpr->get_argName() );
-				alternatives.push_back( Alternative( newExpr.clone(), env, Cost() ) );
-				PRINT(
-					std::cerr << "decl is ";
-					(*i)->print( std::cerr );
-					std::cerr << std::endl;
-					std::cerr << "newExpr is ";
-					newExpr.print( std::cerr );
-					std::cerr << std::endl;
-					)
-					renameTypes( alternatives.back().expr );
-				if ( StructInstType *structInst = dynamic_cast< StructInstType* >( (*i)->get_type() ) ) {
-					addAggMembers( structInst, &newExpr, Cost( 0, 0, 1 ), "" );
-				} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( (*i)->get_type() ) ) {
-					addAggMembers( unionInst, &newExpr, Cost( 0, 0, 1 ), "" );
-				} // if
-			} // for
+		for ( std::list< DeclarationWithType* >::iterator i = declList.begin(); i != declList.end(); ++i ) {
+			VariableExpr newExpr( *i, nameExpr->get_argName() );
+			alternatives.push_back( Alternative( newExpr.clone(), env, Cost() ) );
+			PRINT(
+				std::cerr << "decl is ";
+				(*i)->print( std::cerr );
+				std::cerr << std::endl;
+				std::cerr << "newExpr is ";
+				newExpr.print( std::cerr );
+				std::cerr << std::endl;
+				)
+			renameTypes( alternatives.back().expr );
+			if ( StructInstType *structInst = dynamic_cast< StructInstType* >( (*i)->get_type() ) ) {
+				addAggMembers( structInst, &newExpr, Cost( 0, 0, 1 ), "" );
+			} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( (*i)->get_type() ) ) {
+				addAggMembers( unionInst, &newExpr, Cost( 0, 0, 1 ), "" );
+			} // if
+		} // for
 	}
 
Index: src/ResolvExpr/AlternativeFinder.h
===================================================================
--- src/ResolvExpr/AlternativeFinder.h	(revision 843054c23fcb725d2486e5e42e91b3741bc523b8)
+++ src/ResolvExpr/AlternativeFinder.h	(revision 0f19d763a07f96324b450e9bafd7fdd52807ea0f)
@@ -30,4 +30,5 @@
 		AlternativeFinder( const SymTab::Indexer &indexer, const TypeEnvironment &env );
 		void find( Expression *expr, bool adjust = false );
+		/// Calls find with the adjust flag set; adjustment turns array and function types into equivalent pointer types
 		void findWithAdjustment( Expression *expr );
 		AltList &get_alternatives() { return alternatives; }
Index: src/ResolvExpr/RenameVars.cc
===================================================================
--- src/ResolvExpr/RenameVars.cc	(revision 843054c23fcb725d2486e5e42e91b3741bc523b8)
+++ src/ResolvExpr/RenameVars.cc	(revision 0f19d763a07f96324b450e9bafd7fdd52807ea0f)
@@ -118,5 +118,7 @@
 ///     type->print( std::cout );
 ///     std::cout << std::endl;
+			// copies current name mapping into new mapping
 			mapStack.push_front( mapStack.front() );
+			// renames all "forall" type names to `_${level}_${name}'
 			for ( std::list< TypeDecl* >::iterator i = type->get_forall().begin(); i != type->get_forall().end(); ++i ) {
 				std::ostrstream output;
@@ -125,4 +127,5 @@
 				mapStack.front()[ (*i)->get_name() ] = newname;
 				(*i)->set_name( newname );
+				// ditto for assertion names, the next level in
 				level++;
 				acceptAll( (*i)->get_assertions(), *this );
@@ -132,4 +135,5 @@
 
 	void RenameVars::typeAfter( Type *type ) {
+		// clears name mapping added by typeBefore()
 		if ( ! type->get_forall().empty() ) {
 			mapStack.pop_front();
Index: src/ResolvExpr/RenameVars.h
===================================================================
--- src/ResolvExpr/RenameVars.h	(revision 843054c23fcb725d2486e5e42e91b3741bc523b8)
+++ src/ResolvExpr/RenameVars.h	(revision 0f19d763a07f96324b450e9bafd7fdd52807ea0f)
@@ -25,4 +25,6 @@
 
 namespace ResolvExpr {
+
+	/// Provides a consistent renaming of forall type names in a hierarchy by prefixing them with a unique "level" ID
 	class RenameVars : public Visitor {
 	  public: