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)

1 files changed, 2 insertions, 0 deletions

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.