diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml | 12 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 2 |
2 files changed, 7 insertions, 7 deletions
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;; |