From 5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8 Mon Sep 17 00:00:00 2001
From: Théo Winterhalter
Date: Wed, 26 Sep 2018 11:26:50 +0200
Subject: Combined Scheme tests sort to use either "*" or "/\"

And update documentation.---
 library/coqlib.ml  | 6 ++++++
 library/coqlib.mli | 8 ++++++--
 2 files changed, 12 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 36a9598f36..026b7aa316 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -349,6 +349,9 @@ let coq_iff = lazy_init_reference ["Logic"] "iff"
 let coq_iff_left_proj  = lazy_init_reference ["Logic"] "proj1"
 let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
 
+let coq_prod = lazy_init_reference ["Datatypes"] "prod"
+let coq_pair = lazy_init_reference ["Datatypes"] "pair"
+
 (* Runtime part *)
 let build_coq_True ()  = Lazy.force coq_True
 let build_coq_I ()     = Lazy.force coq_I
@@ -364,6 +367,9 @@ let build_coq_iff ()   = Lazy.force coq_iff
 let build_coq_iff_left_proj ()  = Lazy.force coq_iff_left_proj
 let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 
+let build_coq_prod () = Lazy.force coq_prod
+let build_coq_pair () = Lazy.force coq_pair
+
 
 (* The following is less readable but does not depend on parsing *)
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
diff --git a/library/coqlib.mli b/library/coqlib.mli
index b4bd1b0e06..8844684957 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -101,7 +101,7 @@ val glob_jmeq : GlobRef.t
    at compile time. Therefore, we can only provide methods to build
    them at runtime. This is the purpose of the [constr delayed] and
    [constr_pattern delayed] types. Objects of this time needs to be
-   forced with [delayed_force] to get the actual constr or pattern 
+   forced with [delayed_force] to get the actual constr or pattern
    at runtime. *)
 
 type coq_bool_data = {
@@ -167,7 +167,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 val build_coq_sumbool : GlobRef.t delayed
 
 (** {6 ... } *)
-(** Connectives 
+(** Connectives
    The False proposition *)
 val build_coq_False : GlobRef.t delayed
 
@@ -186,6 +186,10 @@ val build_coq_iff : GlobRef.t delayed
 val build_coq_iff_left_proj : GlobRef.t delayed
 val build_coq_iff_right_proj : GlobRef.t delayed
 
+(** Pairs *)
+val build_coq_prod : GlobRef.t delayed
+val build_coq_pair : GlobRef.t delayed
+
 (** Disjunction *)
 val build_coq_or : GlobRef.t delayed
 
-- 
cgit v1.2.3