diff options
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 41414c96..acd11b45 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -21,7 +21,7 @@ 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)} := +Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := existT _ n H. Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. |