summaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /interp/coqlib.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml11
1 files changed, 3 insertions, 8 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index afee83e8..79a217a1 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *)
open Util
open Pp
@@ -152,12 +152,7 @@ type coq_sigma_data = {
type 'a delayed = unit -> 'a
-let build_sigma_set () =
- { proj1 = init_constant ["Specif"] "projS1";
- proj2 = init_constant ["Specif"] "projS2";
- elim = init_constant ["Specif"] "sigS_rec";
- intro = init_constant ["Specif"] "existS";
- typ = init_constant ["Specif"] "sigS" }
+let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
{ proj1 = init_constant ["Specif"] "projT1";
@@ -257,7 +252,7 @@ let build_coq_ex () = Lazy.force coq_ex
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
-let coq_existS_ref = lazy (init_reference ["Specif"] "existS")
+let coq_existS_ref = lazy (anomaly "use coq_existT_ref")
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
let coq_False_ref = lazy (init_reference ["Logic"] "False")