Fix backtracking heuristic in typeclass resolution.

Now that backtracking is working correctly, we need to avoid a
non-termination issue introduced by the [RelCompFun] definition in
RelationPairs, by adding a [Measure] typeclass. It could be used to have
a uniform notation for measures/interpretations in Numbers and be but in
the interfaces too, only the mimimal change was implemented.
Fix syntax change in test-suite scripts.


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

1 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index a6f1e299b..b4efa7edc 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -1,4 +1,4 @@
-Generalizable Variables all.
+Generalizable All Variables.
 
 Open Scope type_scope.
 
@@ -57,7 +57,7 @@ Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) :=
 Instance BoolCan : interp_pair bool :=
   { repr := Bool ; link := refl_equal _ }.
 
-Instance VarCan : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
+Instance VarCan x : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
 Instance SetCan : interp_pair Set := { repr := SET ; link := refl_equal _ }.
 Instance PropCan : interp_pair Prop := { repr := PROP ; link := refl_equal _ }.
 Instance TypeCan : interp_pair Type := { repr := TYPE ; link := refl_equal _ }.