From 2d1051cc4a1dfdd1a55e2df6ba331d7f1954bb61 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 2 Oct 2019 11:40:38 +0100
Subject: Coq: limited support for existentially-typed tuples - in particular
 at monadic interfaces (i.e., sufficient for instruction   ast types) - see
 commented out part of test/coq/pass/ast_with_dep_tuple.sail for an   example
 that's not currently supported - generate definitions for type-level Bool
 definitions (i.e., predicates)

---
 lib/coq/Sail2_values.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 3b5b9675..5bc630e5 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -46,6 +46,8 @@ End Morphism.
 Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} :=
   existT _ n H.
 
+Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & T' x & ArithFact (P x)} :=
+  existT2 _ _ n m H.
 
 Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness.
 Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness.
-- 
cgit v1.2.3