aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-07 12:42:01 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-07 12:42:01 +0200
commit276f08cb053eed175478c4c9359e61fb949742ba (patch)
treec4d263e69957a528ef7965cd5f66d2652842b436
parent70333c957d42d3da208f442d8e7bed7133b57e5c (diff)
parent0e7e6953e9ee4178d48bf7fa05a7f03d13aa4a6f (diff)
Merge PR #904: Add build_coq_or to API.Coqlib
-rw-r--r--API/API.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli
index d1774afe5..9114df3ea 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2107,6 +2107,7 @@ sig
val coq_not_ref : Globnames.global_reference lazy_t
val coq_or_ref : Globnames.global_reference lazy_t
val build_coq_and : Globnames.global_reference Util.delayed
+ val build_coq_or : Globnames.global_reference Util.delayed
val build_coq_I : Globnames.global_reference Util.delayed
val coq_reference : string -> string list -> string -> Globnames.global_reference
end