From 8aea38ca9b526d1d1ed731948528b4e921b303d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Nov 2003 12:33:06 +0000
Subject: Prise en compte des defs syntaxiques dans is_global et
 global_reference qui passent donc de Termops a Constrintern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml  | 14 --------------
 pretyping/termops.mli |  7 -------
 2 files changed, 21 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 23f9a7ffc7..f9e949c84c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -899,17 +899,3 @@ let rec rename_bound_var env l c =
   | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
   | x -> c
 
-(* References to constr *)
-
-let global_reference id = 
-  constr_of_reference (Nametab.locate (make_short_qualid id))
-
-let construct_reference ctx id =
-  try
-    mkVar (let _ = Sign.lookup_named id ctx in id)
-  with Not_found ->
-    global_reference id
-
-let global_reference_in_absolute_module dir id = 
-  constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id))
-
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index af75cfd2d1..da3033b0c0 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -181,12 +181,5 @@ val make_all_name_different : env -> env
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
-(* References to constr *)
-
-val construct_reference : named_context -> identifier -> constr
-val global_reference : identifier -> constr
-val global_reference_in_absolute_module : dir_path -> identifier -> constr
-
 (* Test if an identifier is the basename of a global reference *)
-val is_global : identifier -> bool
 val is_section_variable : identifier -> bool
-- 
cgit v1.2.3