From a07d4536febf5c5e4a7c635b01195e6b6036724b Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 25 Jan 2006 14:44:54 +0000
Subject: exporting the global  reference to the inductive " \/  " in coqlib
 and eq_rawconstr  in topconstr  to  prepare the  introduction  of the  new
 version of functionnal induction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/coqlib.ml     | 1 +
 interp/coqlib.mli    | 2 ++
 interp/topconstr.mli | 2 ++
 3 files changed, 5 insertions(+)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 785291b84e..b8a93cf3a5 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -251,4 +251,5 @@ let coq_not_ref     = lazy (init_reference ["Logic"] "not")
 let coq_False_ref   = lazy (init_reference ["Logic"] "False")
 let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
 let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
+let coq_or_ref     = lazy (init_reference ["Logic"] "or")
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 2d25228058..0848c30846 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -123,3 +123,5 @@ val coq_not_ref : global_reference lazy_t
 val coq_False_ref : global_reference lazy_t
 val coq_sumbool_ref : global_reference lazy_t
 val coq_sig_ref : global_reference lazy_t
+
+val coq_or_ref : global_reference lazy_t
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d6f7dbd037..11475cdaa2 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -53,6 +53,8 @@ val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr
 
 val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
 
+val eq_rawconstr : rawconstr -> rawconstr -> bool
+
 (* [match_aconstr metas] match a rawconstr against an aconstr with
    metavariables in [metas]; it raises [No_match] if the matching fails *)
 exception No_match
-- 
cgit v1.2.3