From 10fa54f60acdfc8de6b59659f9fa8bc1ed3c18e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 28 May 2006 16:21:04 +0000
Subject: - Déplacement des types paramétriques prod, sum, option, identity,  
 sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers
 les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau
 sigT2 - Changements en conséquence dans les théories (notamment
 Field_Tactic),   ainsi que dans les modules ML
 Coqlib/Equality/Hipattern/Field

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/coqlib.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index f9a1c6466f..cfde102021 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -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")
-- 
cgit v1.2.3