* Bug fix: in case of non dependent implications the second argument was

  not correctly de-lifted.
* [EXPERIMENTAL]: the Add Relation and Add Morphism commands now accept also
  quantified relations and quantified morphisms. [ Add Setoid doesn't do that
  yet. ] However, in case of quantified relations the matching between
  an argument type and the (quantified) carrier expected for it is quite weak
  and is complete only not modulus conversion.
* Many bugs have probably been introduced by the experimental feature.
  However, the bugs should manifest only in the case of quantified relations.
  In particular Leibniz has a strange status and its management should be
  revised.
* Open problem: should the data type for relations and morphisms be changed
  to explicitly show the quantifications?


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

0 files changed, 0 insertions, 0 deletions