diff options
| author | filliatr | 2001-10-12 07:56:19 +0000 |
|---|---|---|
| committer | filliatr | 2001-10-12 07:56:19 +0000 |
| commit | 2367f109b226070e530f4f05ec644e5fc82ab63e (patch) | |
| tree | d4493dfb65603facf6818973dd715377e5e437f5 /contrib/interface | |
| parent | 301a70e45eac43f034077c95bce04edbcf2ab4ad (diff) | |
reparation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2110 85f007b7-540e-0410-9357-904b9bb8a0f7
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;; |