From 091bfff6ce37a303550e79abb23fdc992a28f7e3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 3 Nov 2020 02:11:33 +0100
Subject: Fixes #13298: primitive projections needs a correct typing
 environment.

---
 test-suite/output/Search_bug13298.out | 1 +
 test-suite/output/Search_bug13298.v   | 3 +++
 2 files changed, 4 insertions(+)
 create mode 100644 test-suite/output/Search_bug13298.out
 create mode 100644 test-suite/output/Search_bug13298.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/Search_bug13298.out b/test-suite/output/Search_bug13298.out
new file mode 100644
index 0000000000..18488c790f
--- /dev/null
+++ b/test-suite/output/Search_bug13298.out
@@ -0,0 +1 @@
+snd: forall c : c, fst c = 0
diff --git a/test-suite/output/Search_bug13298.v b/test-suite/output/Search_bug13298.v
new file mode 100644
index 0000000000..9a75321c64
--- /dev/null
+++ b/test-suite/output/Search_bug13298.v
@@ -0,0 +1,3 @@
+Set Primitive Projections.
+Record c : Type := { fst : nat; snd : fst = 0 }.
+Search concl:fst.
-- 
cgit v1.2.3