From affdf7a0b6fa9a49562f4af04903ae8e44237654 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Mon, 25 Feb 2013 23:02:20 +0000
Subject: Evarconv: When doing a iota of a fixpoint, use constant name instead
 of fixpoint definition

+ Help the use of #trace on evar_conv_appr_x

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/inference.out | 2 ++
 test-suite/output/inference.v   | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'test-suite')

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).
-- 
cgit v1.2.3