2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index bca3b361ac..16b23ed18d 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,3 +4,5 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
+fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
+     : forall m n p : nat, S m <= S n + p -> m <= n + p
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 968ea71a94..fe537c59a7 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -12,3 +12,6 @@ Definition P (e:option L) :=
   end.
 
 Print P.
+
+(* Check that plus is folded even if reduction is involved *)
+Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).