diff options
| -rw-r--r-- | contrib/correctness/pdb.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/perror.ml | 2 | ||||
| -rw-r--r-- | contrib/correctness/pmisc.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml index 3aeb876ddb..46d86a3f6b 100644 --- a/contrib/correctness/pdb.ml +++ b/contrib/correctness/pdb.ml @@ -21,7 +21,7 @@ open Penv let cci_global id = try - Declare.global_reference id + global_reference id with _ -> raise Not_found diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml index 19b4db9928..18498377fb 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' = Declare.global_reference id in + let c' = Termops.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 60f7306ac5..ca7cee2e2e 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 = id_of_string s in - Declare.global_reference id + Termops.global_reference id let connective_and = id_of_string "prog_bool_and" let connective_or = id_of_string "prog_bool_or" |