Imported Upstream version 8.6upstream/8.6

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8d942d90..06511ace 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -465,12 +465,12 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     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 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