diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 39 |
1 files changed, 21 insertions, 18 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 1d5619969..78e549e13 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -22,6 +22,7 @@ open Astterm open Environ open Pattern open Printer +open Libnames open Nametab (* The functions print_constructors and crible implement the behavior needed @@ -49,9 +50,9 @@ let rec head_const c = match kind_of_term c with let crible (fn : global_reference -> env -> constr -> unit) ref = let env = Global.env () in - let imported = Library.opened_modules() in + let imported = Library.opened_libraries() in let const = constr_of_reference ref in - let crible_rec sp lobj = + let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try @@ -60,26 +61,28 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = with Not_found -> (* we are in a section *) ()) | "CONSTANT" | "PARAMETER" -> - let {const_type=typ} = Global.lookup_constant sp in - if (head_const typ) = const then fn (ConstRef sp) env typ + let kn=locate_constant (qualid_of_sp sp) in + let {const_type=typ} = Global.lookup_constant kn in + if (head_const typ) = const then fn (ConstRef kn) env typ | "INDUCTIVE" -> - let mib = Global.lookup_mind sp in - let arities = + let kn=locate_mind (qualid_of_sp sp) in + let mib = Global.lookup_mind kn in +(* let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) - mib.mind_packets in + mib.mind_packets in*) (match kind_of_term const with - | Ind ((sp',tyi) as indsp) -> - if sp=sp' then - print_constructors indsp fn env mib.mind_packets.(tyi) + | Ind ((kn',tyi) as ind) -> + if kn=kn' then + print_constructors ind fn env mib.mind_packets.(tyi) | _ -> ()) | _ -> () in - try - Library.iter_all_segments false crible_rec - with Not_found -> - errorlabstrm "search" + try + Declaremods.iter_all_segments false crible_rec + with Not_found -> + errorlabstrm "search" (pr_global ref ++ spc () ++ str "not declared") (* Fine Search. By Yves Bertot. *) @@ -104,9 +107,9 @@ let plain_display ref a c = msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) let filter_by_module (module_list:dir_path list) (accept:bool) - (ref:global_reference) (env:env) _ = + (ref:global_reference) _ _ = try - let sp = sp_of_global env ref in + let sp = sp_of_global None ref in let sl = dirpath sp in let rec filter_aux = function | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) @@ -117,9 +120,9 @@ let filter_by_module (module_list:dir_path list) (accept:bool) false let gref_eq = - IndRef (make_path Coqlib.logic_module (id_of_string "eq"), 0) + IndRef (Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0) let gref_eqT = - IndRef (make_path Coqlib.logic_type_module (id_of_string "eqT"), 0) + IndRef (Libnames.encode_kn Coqlib.logic_type_module (id_of_string "eqT"), 0) let mk_rewrite_pattern1 eq pattern = PApp (PRef eq, [| PMeta None; pattern; PMeta None |]) |