From 045c85f66a65c6aaedeed578d352c6de27d5e6a4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:37:23 +0000
Subject: Centralisation des références à des globaux de Coq dans Coqlib
 (ex-Stdlib) et suppression Stock

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1380 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/stdlib.ml | 17 -----------------
 1 file changed, 17 deletions(-)
 delete mode 100644 parsing/stdlib.ml

(limited to 'parsing/stdlib.ml')

diff --git a/parsing/stdlib.ml b/parsing/stdlib.ml
deleted file mode 100644
index 8c4e2bf681..0000000000
--- a/parsing/stdlib.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-
-(* $Id$ *)
-
-open Names
-open Term
-open Declare
-
-let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
-let myvar_path =
-  make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
-
-let glob_nat = IndRef (nat_path,0)
-
-let glob_O = ConstructRef ((nat_path,0),1)
-let glob_S = ConstructRef ((nat_path,0),2)
-
-let glob_My_special_variable_nat = ConstRef myvar_path
-- 
cgit v1.2.3