tabareau/Forcing — pull request #11 by tabareau (2012-06-14 14:57:24+00:00)
Title: Prop and Types

* The translation now returns the sort of types it translates, so that it is know if we're building exists or existsT values and we can use the right projections.
* Avoid requiring trivial commutativity properties when we're in Prop! The interpretation of forall should be changed in the paper in particular.
* Fix translation of applications which was wrong for applications with more than one argument.