From bc45a06c67e217bdc1aa86008b65451748b4cf1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Mar 2004 17:46:45 +0000
Subject: Branchement EmptyT, UnitT, IT vers leur equivalent dans Set

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

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index b684036344..6f3ec63deb 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -208,12 +208,18 @@ let build_coq_idT_data () = {
   congr = Lazy.force coq_idT_congr;
   sym  = Lazy.force coq_idT_sym }
 
+let lazy_init_constant_v7 d id id7 =
+  if !Options.v7 then lazy_init_constant d id else 
+  lazy (anomaly
+   (id7^" does no longer exist in V8 new syntax, use "^id
+    ^" instead (probably an error in ML contributed code)"))
+
 (* Empty Type *)
-let coq_EmptyT = lazy_init_constant ["Logic_Type"] "EmptyT"
+let coq_EmptyT = lazy_init_constant_v7 ["Logic"] "False" "EmptyT"
 
 (* Unit Type and its unique inhabitant *)
-let coq_UnitT  = lazy_init_constant ["Logic_Type"] "UnitT"
-let coq_IT     = lazy_init_constant ["Logic_Type"] "IT"
+let coq_UnitT  = lazy_init_constant_v7 ["Datatypes"] "unit" "UnitT"
+let coq_IT     = lazy_init_constant_v7 ["Datatypes"] "tt" "IT"
 
 (* The False proposition *)
 let coq_False  = lazy_init_constant ["Logic"] "False"
-- 
cgit v1.2.3