Improved tactic "order" in OrderedType

 I forgot to mention in last commit message about MSets that
 the corresponding OrderedType2 comes with a redesigned "order"
 tactic. It should now be complete for its purpose (that is
 solve systems of (in)equations of variables over == < <= <>).
 Non-linear matching is cool, I love Ltac :-). Unlike the old "order",
 this new version is meant to completely solve the goal or fail.
 Speed might be an issue for big systems, but in pratice it is
 quite efficient on the examples encountered in FSets.

 This commit:
  - propagages this new "order" to the original OrderedType.v file
    used for the old FSet.
  - fixes a bug : the ltac loop shouldn't fail otherwise strange
    backtrack occurs. I hate Ltac :-(

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

0 files changed, 0 insertions, 0 deletions