A try at using sort variables during unification. Instead of refreshing

universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort 
constraints are thrown away at the end of unification for the moment, 
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions