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 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml | 12 | ||||
| -rw-r--r-- | 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;; |
