diff options
Diffstat (limited to 'interp/coqlib.mli')
| -rw-r--r-- | interp/coqlib.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli index ed5e46c1a..098dad1d5 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -94,6 +94,8 @@ type coq_sigma_data = { val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed +(* Non-dependent pairs in Set from Datatypes *) +val build_prod : coq_sigma_data delayed type coq_leibniz_eq_data = { eq : constr; |