3 files changed, 3 insertions, 2 deletions
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 46d86a3f6b..28327ee27e 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -14,6 +14,7 @@ open Names
 open Term
 open Termops
 open Nametab
+open Constrintern
 
 open Ptype
 open Past
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 18498377fb..3d802c4e70 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -66,7 +66,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' = Termops.global_reference id in
+      let c' = Constrintern.global_reference id in
       Reductionops.is_conv (Global.env()) Evd.empty c c'
   | _ -> false 
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index ba96b98b71..5fbcf4489f 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -170,7 +170,7 @@ let coq_false = mkConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = Constrextern.id_of_v7_string s in
-  Termops.global_reference id
+  Constrintern.global_reference id
 
 let connective_and = id_of_string "prog_bool_and"
 let connective_or  = id_of_string "prog_bool_or"