From 6b485cb062f474454b467c53edff69b10f6d3b5f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Jun 2018 16:06:05 +0100
Subject: Coq: some very basic existential support Only single variable in
 places, only packed at literals and variables, no unpacking

---
 lib/coq/Sail_values.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail_values.v
index 0dc25e1b..2343490b 100644
--- a/lib/coq/Sail_values.v
+++ b/lib/coq/Sail_values.v
@@ -19,6 +19,9 @@ Lemma use_ArithFact {P} `(ArithFact P) : P.
 apply fact.
 Defined.
 
+Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
+  existT _ n H.
+
 
 Definition ii := Z.
 Definition nn := nat.
-- 
cgit v1.2.3