From 2367f109b226070e530f4f05ec644e5fc82ab63e Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 12 Oct 2001 07:56:19 +0000
Subject: reparation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/pdb.ml    |  2 +-
 contrib/correctness/perror.ml |  2 +-
 contrib/correctness/pmisc.ml  |  2 +-
 contrib/interface/centaur.ml  | 12 ++++++------
 contrib/interface/pbp.ml      |  2 +-
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 7ad6a79dba..a0651e90c2 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -19,7 +19,7 @@ open Penv
 
 let cci_global id =
   try
-    Declare.global_reference CCI id
+    Declare.global_reference id
   with
     _ -> raise Not_found
 
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 950bc62bfa..1eb44d5bc5 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -65,7 +65,7 @@ let check_for_array loc id = function
 let is_constant_type s = function
     TypePure c ->
       let id = id_of_string s in
-      let c' = Declare.global_reference CCI id in
+      let c' = Declare.global_reference id in
       Reduction.is_conv (Global.env()) Evd.empty c c'
   | _ -> false 
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 936c39d565..60fe808e0f 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -151,7 +151,7 @@ let coq_false = mkMutConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = id_of_string s in
-  Declare.global_reference CCI id
+  Declare.global_reference id
 
 let connective_and = id_of_string "prog_bool_and"
 let connective_or  = id_of_string "prog_bool_or"
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 4e069c11cf..2f864b13ee 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -590,12 +590,12 @@ let command_changes = [
    function
        (VARG_QUALID qid)::l ->
          (fun () -> 
-           ctv_SEARCH_LIST:=[];
-	    let global_ref = Vernacentries.global dummy_loc qid in
-           filtered_search
-             (filter_by_module_from_varg_list l)
-	     add_search (Nametab.locate qid);
-	   search_output_results())
+            ctv_SEARCH_LIST:=[];
+	    let global_ref = Nametab.global dummy_loc qid in
+            filtered_search
+              (filter_by_module_from_varg_list l)
+	      add_search (Nametab.locate qid);
+	    search_output_results())
      |	_ -> failwith "bad form of arguments");
 
   ("SearchRewrite",
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 409f5eb368..cefc9f7e07 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -185,7 +185,7 @@ let reference dir s =
 	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
 let constant dir s =
-  Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s);;
+  Declare.constr_of_reference (reference dir s);;
 
 
 let andconstr: unit -> constr = Coqlib.build_coq_and;;
-- 
cgit v1.2.3