From eb72574e1b526827706ee06206eb4a9626af3236 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 28 Jun 2016 10:27:03 +0200
Subject: Typeclasses: use once in by clause for typeclass eauto

Otherwise we may backtrack on the resolution in a
by which seems strange.
---
 theories/Classes/Morphisms.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 607e7d10c5..06511ace57 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -470,7 +470,7 @@ Ltac partial_application_tactic :=
     end
   in
   let rec do_partial H ar m := 
-    match ar with
+    lazymatch ar with
       | 0%nat => do_partial_apps H m ltac:(fail 1)
       | S ?n' =>
         match m with
@@ -483,7 +483,7 @@ Ltac partial_application_tactic :=
      let n := fresh in evar (n:nat) ;
      let v := eval compute in n in clear n ;
       let H := fresh in
-        assert(H:Params m' v) by (subst m'; typeclasses eauto) ;
+        assert(H:Params m' v) by (subst m'; once typeclasses eauto) ;
           let v' := eval compute in v in subst m';
             (sk H v' || fail 1))
     || fk
-- 
cgit v1.2.3