aboutsummaryrefslogtreecommitdiffhomepage
path: root/API
diff options
context:
space:
mode:
authorGravatar Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de>2017-07-20 18:33:46 +0200
committerGravatar Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de>2017-08-07 11:44:35 +0200
commit0e7e6953e9ee4178d48bf7fa05a7f03d13aa4a6f (patch)
treea0449928105e302978093b189ceeb96470a94f64 /API
parent1f46ff6db53c2ca471d9ea067d0824755b2f34da (diff)
Add build_coq_or to API
Diffstat (limited to 'API')
-rw-r--r--API/API.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli
index a0e77edd1..356456f73 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