diff options
| author | herbelin | 2004-03-11 17:46:45 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-11 17:46:45 +0000 |
| commit | bc45a06c67e217bdc1aa86008b65451748b4cf1b (patch) | |
| tree | 38e242d50a06aa78807add177d9d50ccdff1b8b0 /interp | |
| parent | 106b3a4fd1b7c854fcfdab431b9d69fc43d1b215 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 12 |
1 files 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" |