aboutsummaryrefslogtreecommitdiffstats
path: root/src/classes
diff options
context:
space:
mode:
Diffstat (limited to 'src/classes')
-rw-r--r--src/classes/SMT_classes.v9
-rw-r--r--src/classes/SMT_classes_instances.v9
2 files changed, 18 insertions, 0 deletions
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 1c050c9..9a33271 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -217,3 +217,12 @@ Section CompDec_from.
Typ_compdec T CompDec_from.
End CompDec_from.
+
+
+(* Register constants for OCaml access *)
+Register typ_compdec as SMTCoq.classes.SMT_classes.typ_compdec.
+Register Typ_compdec as SMTCoq.classes.SMT_classes.Typ_compdec.
+Register te_carrier as SMTCoq.classes.SMT_classes.te_carrier.
+Register te_compdec as SMTCoq.classes.SMT_classes.te_compdec.
+Register eqb_of_compdec as SMTCoq.classes.SMT_classes.eqb_of_compdec.
+Register CompDec as SMTCoq.classes.SMT_classes.CompDec.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 1c8b2f6..0e51366 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -747,3 +747,12 @@ Section prod.
|}.
End prod.
+
+
+(* Register constants for OCaml access *)
+Register unit_typ_compdec as SMTCoq.classes.SMT_classes_instances.unit_typ_compdec.
+Register bool_compdec as SMTCoq.classes.SMT_classes_instances.bool_compdec.
+Register Z_compdec as SMTCoq.classes.SMT_classes_instances.Z_compdec.
+Register Positive_compdec as SMTCoq.classes.SMT_classes_instances.Positive_compdec.
+Register BV_compdec as SMTCoq.classes.SMT_classes_instances.BV_compdec.
+Register FArray_compdec as SMTCoq.classes.SMT_classes_instances.FArray_compdec.