From c54142e48402d36f0b69239612bf04c1e5bd9ee4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 8 Nov 2007 22:22:16 +0000 Subject: Prise en compte des notations "alias" dans la globalisation des coercions. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/dp/dp.ml | 4 +-- contrib/funind/indfun_common.ml | 2 +- contrib/recdef/recdef.ml4 | 36 +++++++++++++-------------- contrib/setoid_ring/newring.ml4 | 6 +++-- contrib/subtac/subtac_command.ml | 4 +-- interp/syntax_def.ml | 18 +++++++++++--- interp/syntax_def.mli | 17 +++++++++---- library/libnames.ml | 2 ++ library/libnames.mli | 2 ++ library/nametab.ml | 4 +-- library/nametab.mli | 4 +-- pretyping/classops.ml | 6 ++--- pretyping/detyping.ml | 11 ++------- pretyping/detyping.mli | 2 -- tactics/auto.ml | 10 ++++---- tactics/decl_interp.ml | 2 +- tactics/decl_proof_instr.ml | 2 +- tactics/tacinterp.ml | 16 ++++++------ toplevel/command.ml | 6 ++--- toplevel/vernacentries.ml | 53 +++++++++++++++------------------------- toplevel/whelp.ml4 | 10 ++------ 21 files changed, 106 insertions(+), 111 deletions(-) diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index b5ba3b00e..22fefa65d 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -443,7 +443,7 @@ and axiomatize_body env r id d = match r with | IndRef i -> iter_all_constructors i (fun _ c -> - let rc = reference_of_constr c in + let rc = global_of_constr c in try begin match tr_global env rc with | DeclFun (_, _, [], _) -> () @@ -460,7 +460,7 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with iter_all_constructors ci.ci_ind (fun j cj -> try - let cjr = reference_of_constr cj in + let cjr = global_of_constr cj in begin match tr_global env cjr with | DeclFun (idc, _, l, _) -> let b = br.(j) in diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 13b242d5d..609504ba5 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -131,7 +131,7 @@ let coq_constant s = (Coqlib.init_modules @ Coqlib.arith_modules) s;; let constant sl s = - constr_of_reference + constr_of_global (Nametab.locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) (id_of_string s)));; diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 832e4647f..318cde773 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -236,7 +236,7 @@ let coq_constant s = (Coqlib.init_modules @ Coqlib.arith_modules) s;; let constant sl s = - constr_of_reference + constr_of_global (locate (make_qualid(Names.make_dirpath (List.map id_of_string (List.rev sl))) (id_of_string s)));; @@ -275,8 +275,8 @@ let acc_inv_id = function () -> (coq_constant "Acc_inv") let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof") let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded") let max_ref = function () -> (find_reference ["Recdef"] "max") -let iter = function () -> (constr_of_reference (delayed_force iter_ref)) -let max_constr = function () -> (constr_of_reference (delayed_force max_ref)) +let iter = function () -> (constr_of_global (delayed_force iter_ref)) +let max_constr = function () -> (constr_of_global (delayed_force max_ref)) let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" @@ -622,7 +622,7 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr = - match find_call_occs 0 (mkVar (get_f (constr_of_reference func))) expr with + match find_call_occs 0 (mkVar (get_f (constr_of_global func))) expr with | context_fn, args -> observe_tac "introduce_all_values" (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] []) @@ -669,13 +669,13 @@ let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier) proveterminate let hyp_terminates nb_args func = - let a_arrow_b = arg_type (constr_of_reference func) in + let a_arrow_b = arg_type (constr_of_global func) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = mkApp(delayed_force iter, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: - constr_of_reference func::mkRel 1:: + constr_of_global func::mkRel 1:: List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args) ) ) @@ -798,7 +798,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a begin fun g -> let ids = ids_of_named_context (pf_hyps g) in - let func_body = (def_of_const (constr_of_reference func)) in + let func_body = (def_of_const (constr_of_global func)) in let (f_name, _, body1) = destLambda func_body in let f_id = match f_name with @@ -864,7 +864,7 @@ let build_and_l l = let c,tac,nb = f pl in mk_and p1 c, tclTHENS - (apply (constr_of_reference conj_constr)) + (apply (constr_of_global conj_constr)) [tclIDTAC; tac ],nb+1 @@ -1090,7 +1090,7 @@ let rec n_x_id ids n = let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:identifier list -> tactic) g = let ids = pf_ids_of_hyps g in - let terminate_constr = constr_of_reference term_f in + let terminate_constr = constr_of_global term_f in let nargs = nb_prod (type_of_const terminate_constr) in let x = n_x_id ids nargs in tclTHENLIST [ @@ -1136,7 +1136,7 @@ let rec introduce_all_values_eq cont_tac functional termine (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); unfold_in_hyp [([1], evaluable_of_global_reference - (reference_of_constr functional))] + (global_of_constr functional))] (([], heq2), Tacexpr.InHyp); tclTHENS (fun gls -> @@ -1260,7 +1260,7 @@ let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) fun g -> let ids = ids_of_named_context (pf_hyps g) in rec_leaf_eq termine f ids - (constr_of_reference functional) + (constr_of_global functional) eqs expr fn args g)) | _ -> (match find_call_occs 0 f expr with @@ -1269,7 +1269,7 @@ let rec prove_eq (termine:constr) (f:constr)(functional:global_reference) fun g -> let ids = ids_of_named_context (pf_hyps g) in observe_tac "rec_leaf_eq" (rec_leaf_eq - termine f ids (constr_of_reference functional) + termine f ids (constr_of_global functional) eqs expr fn args) g));; let (com_eqn : identifier -> @@ -1285,7 +1285,7 @@ let (com_eqn : identifier -> | _ -> anomaly "terminate_lemma: not a constant" in let (evmap, env) = Command.get_current_context() in - let f_constr = (constr_of_reference f_ref) in + let f_constr = (constr_of_global f_ref) in let equation_lemma_type = subst1 f_constr equation_lemma_type in (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); @@ -1293,12 +1293,12 @@ let (com_eqn : identifier -> (start_equation f_ref terminate_ref (fun x -> prove_eq - (constr_of_reference terminate_ref) + (constr_of_global terminate_ref) f_constr functional_ref [] (instantiate_lambda - (def_of_const (constr_of_reference functional_ref)) + (def_of_const (constr_of_global functional_ref)) (f_constr::List.map mkVar x) ) ) @@ -1371,9 +1371,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num if not !stop then let eq_ref = Nametab.locate (make_short_qualid equation_id ) in - let f_ref = destConst (constr_of_reference f_ref) - and functional_ref = destConst (constr_of_reference functional_ref) - and eq_ref = destConst (constr_of_reference eq_ref) in + let f_ref = destConst (constr_of_global f_ref) + and functional_ref = destConst (constr_of_global functional_ref) + and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; if Options.is_verbose () diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 649db86ce..1cbae1e2f 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -565,7 +565,8 @@ type cst_tac_spec = let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = match cst_tac with Some (CstTac t) -> Tacinterp.glob_tactic t - | Some (Closed lc) -> closed_term_ast (List.map Nametab.global lc) + | Some (Closed lc) -> + closed_term_ast (List.map Syntax_def.global_with_alias lc) | None -> (match rk, opp, kind with Abstract, None, _ -> @@ -608,7 +609,8 @@ let interp_power env pow = let tac = match tac with | CstTac t -> Tacinterp.glob_tactic t - | Closed lc -> closed_term_ast (List.map Nametab.global lc) in + | Closed lc -> + closed_term_ast (List.map Syntax_def.global_with_alias lc) in let spec = make_hyp env (ic spec) in (tac, lapp coq_Some [|carrier; spec|]) diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 9cbfb0246..d7d304279 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -287,7 +287,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let fix_def = match measure_fn with None -> - mkApp (constr_of_reference (Lazy.force fix_sub_ref), + mkApp (constr_of_global (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; make_existential dummy_loc ~opaque:false env isevars wf_proof ; @@ -295,7 +295,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = lift lift_cst intern_body_lam |]) | Some f -> lift (succ after_length) - (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), + (mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), [| argtyp ; f ; lift lift_cst prop ; diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 3769362b1..b81e7e6c8 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -79,14 +79,24 @@ let rec set_loc loc _ a = let search_syntactic_definition loc kn = set_loc loc () (KNmap.find kn !syntax_table) -exception BoundToASyntacticDefThatIsNotARef - -let locate_global qid = +let locate_global_with_alias (loc,qid) = match Nametab.extended_locate qid with | TrueGlobal ref -> ref | SyntacticDef kn -> match search_syntactic_definition dummy_loc kn with | Rawterm.RRef (_,ref) -> ref | _ -> - errorlabstrm "" (pr_qualid qid ++ + user_err_loc (loc,"",pr_qualid qid ++ str " is bound to a notation that does not denote a reference") + +let inductive_of_reference_with_alias r = + match locate_global_with_alias (qualid_of_reference r) with + | IndRef ind -> ind + | ref -> + user_err_loc (loc_of_reference r,"global_inductive", + pr_reference r ++ spc () ++ str "is not an inductive type") + +let global_with_alias r = + let (loc,qid as lqid) = qualid_of_reference r in + try locate_global_with_alias lqid + with Not_found -> Nametab.error_global_not_found_loc loc qid diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 50f2f3e7d..e83cb8885 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,6 +13,7 @@ open Util open Names open Topconstr open Rawterm +open Libnames (*i*) (* Syntactic definitions. *) @@ -23,10 +24,16 @@ val declare_syntactic_definition : bool -> identifier -> bool -> aconstr val search_syntactic_definition : loc -> kernel_name -> rawconstr -(* [locate_global] locates global reference possibly following a chain of - syntactic aliases; raise Not_found if not bound in the global env; - raise an error if bound to a syntactic def that does not denote a - reference *) +(* [locate_global_with_alias] locates global reference possibly following + a notation if this notation has a role of aliasing; raise Not_found + if not bound in the global env; raise an error if bound to a + syntactic def that does not denote a reference *) -val locate_global : Libnames.qualid -> Libnames.global_reference +val locate_global_with_alias : qualid located -> global_reference + +(* Locate a reference taking into account possible "alias" notations *) +val global_with_alias : reference -> global_reference + +(* The same for inductive types *) +val inductive_of_reference_with_alias : reference -> inductive diff --git a/library/libnames.ml b/library/libnames.ml index dcdd5ac41..4d25c42f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -49,8 +49,10 @@ let constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp +(* let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr +*) module RefOrdered = struct diff --git a/library/libnames.mli b/library/libnames.mli index fe5033d73..6c6d435be 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -34,9 +34,11 @@ val constr_of_global : global_reference -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> global_reference +(* (* Obsolete synonyms for constr_of_global and global_of_constr *) val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference +*) module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference diff --git a/library/nametab.ml b/library/nametab.ml index ffca8bf4a..395b2159f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -427,7 +427,7 @@ let global r = | TrueGlobal ref -> ref | SyntacticDef _ -> user_err_loc (loc,"global", - str "Unexpected reference to a syntactic definition: " ++ + str "Unexpected reference to a notation: " ++ pr_qualid qid) with Not_found -> error_global_not_found_loc loc qid @@ -497,7 +497,7 @@ let pr_global_env env ref = let s = string_of_qualid (shortest_qualid_of_global env ref) in (str s) -let global_inductive r = +let inductive_of_reference r = match global r with | IndRef ind -> ind | ref -> diff --git a/library/nametab.mli b/library/nametab.mli index 2f6e9e8cb..66de6a708 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -89,9 +89,9 @@ val locate : qualid -> global_reference val global : reference -> global_reference (* The same for inductive types *) -val global_inductive : reference -> inductive +val inductive_of_reference : reference -> inductive -(* This locates also syntactic definitions *) +(* This locates also syntactic definitions; raise [Not_found] if not found *) val extended_locate : qualid -> extended_global_reference (* This locates all names with a given suffix, if qualid is valid as diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 49147dfd7..9a628b3fd 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -370,8 +370,8 @@ let classes () = Bijint.dom !class_tab let coercions () = Gmap.rng !coercion_tab let inheritance_graph () = Gmap.to_list !inheritance_graph -let coercion_of_qualid qid = - let ref = Nametab.global qid in +let coercion_of_reference r = + let ref = Nametab.global r in if not (coercion_exists ref) then errorlabstrm "try_add_coercion" (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion"); @@ -380,7 +380,7 @@ let coercion_of_qualid qid = module CoercionPrinting = struct type t = coe_typ - let encode = coercion_of_qualid + let encode = coercion_of_reference let subst = subst_coe_typ let printer x = pr_global_env Idset.empty x let key = Goptions.SecondaryTable ("Printing","Coercion") diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 049c93641..829c5f404 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -31,8 +31,8 @@ let dl = dummy_loc (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive qid = - let indsp = global_inductive qid in +let encode_inductive r = + let indsp = inductive_of_reference r in let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) @@ -108,13 +108,6 @@ module PrintingCasesLet = module PrintingIf = Goptions.MakeRefTable(PrintingCasesIf) module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) -let force_let ci = - let indsp = ci.ci_ind in - let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc) -let force_if ci = - let indsp = ci.ci_ind in - let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc) - (* Options for printing or not wildcard and synthetisable types *) open Goptions diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 445c2183d..588bc8c84 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -50,8 +50,6 @@ val lookup_index_as_renamed : env -> constr -> int -> int option val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool -val force_if : case_info -> bool -val force_let : case_info -> bool (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/tactics/auto.ml b/tactics/auto.ml index f07541912..a3ac17b34 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -412,8 +412,8 @@ let add_hints local dbnames0 h = | HintsImmediate lhints -> add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> - let f qid = - let r = Nametab.global qid in + let f r = + let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in let r' = match r with | ConstRef c -> EvalConstRef c | VarRef c -> EvalVarRef c @@ -427,7 +427,7 @@ let add_hints local dbnames0 h = | HintsConstructors lqid -> let add_one qid = let env = Global.env() and sigma = Evd.empty in - let isp = global_inductive qid in + let isp = inductive_of_reference qid in let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in @@ -893,8 +893,8 @@ let superauto n to_add argl = let default_superauto g = superauto !default_search_depth [] [] g -let interp_to_add gl locqid = - let r = Nametab.global locqid in +let interp_to_add gl r = + let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in let id = id_of_global r in (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r) diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 02c688e25..ec8a38501 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -153,7 +153,7 @@ let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) +let _eq = Libnames.constr_of_global (Coqlib.glob_eq) let decompose_eq env id = let typ = Environ.named_type id env in diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 134f018ca..1d5ab017c 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -530,7 +530,7 @@ let instr_cut mkstat _thus _then cut gls0 = (* iterated equality *) -let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) +let _eq = Libnames.constr_of_global (Coqlib.glob_eq) let decompose_eq id gls = let typ = pf_get_hyp_typ gls id in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index abe06e5d3..11d86630b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -383,7 +383,7 @@ let loc_of_by_notation f = function let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let intern_inductive_or_by_notation = function - | AN r -> Nametab.global_inductive r + | AN r -> Nametab.inductive_of_reference r | ByNotation (loc,ntn) -> destIndRef (Notation.interp_notation_as_global_reference loc (function IndRef ind -> true | _ -> false) ntn) @@ -395,9 +395,9 @@ let intern_inductive ist = function let intern_global_reference ist = function | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) | r -> - let loc,qid = qualid_of_reference r in - try ArgArg (loc,locate_global qid) - with _ -> + let loc,qid as lqid = qualid_of_reference r in + try ArgArg (loc,locate_global_with_alias lqid) + with Not_found -> error_global_not_found_loc loc qid let intern_tac_ref ist = function @@ -420,8 +420,8 @@ let intern_constr_reference strict ist = function | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist -> RVar (dloc,id), None | r -> - let loc,qid = qualid_of_reference r in - RRef (loc,locate_global qid), if strict then None else Some (CRef r) + let loc,_ as lqid = qualid_of_reference r in + RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) let intern_reference strict ist r = (try Reference (intern_tac_ref ist r) @@ -512,8 +512,8 @@ let short_name = function | _ -> None let interp_global_reference r = - let loc,qid = qualid_of_reference r in - try locate_global qid + let loc,qid as lqid = qualid_of_reference r in + try locate_global_with_alias lqid with Not_found -> match r with | Ident (loc,id) when not !strict_check -> VarRef id diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b9f76d95..99f9e3ed7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -853,7 +853,7 @@ requested let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> - let ind = mkInd (Nametab.global_inductive y) in + let ind = mkInd (Nametab.inductive_of_reference y) in let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) in let z' = family_of_sort (interp_sort z) in @@ -892,7 +892,7 @@ let build_induction_scheme lnamedepindsort = let lrecspec = List.map (fun (_,dep,indid,sort) -> - let ind = Nametab.global_inductive indid in + let ind = Nametab.inductive_of_reference indid in let (mib,mip) = Global.lookup_inductive ind in (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort @@ -921,7 +921,7 @@ tried to declare different schemes at once *) else ( if ischeme <> [] then build_induction_scheme ischeme; List.iter ( fun indname -> - let ind = Nametab.global_inductive indname + let ind = Nametab.inductive_of_reference indname in declare_eq_scheme (fst ind); make_eq_decidability ind ) escheme diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1eb1f8986..784cabcd5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -35,6 +35,7 @@ open Decl_kinds open Topconstr open Pretyping open Redexpr +open Syntax_def (* Pcoq hooks *) @@ -58,7 +59,7 @@ let set_pcoq_hook f = pcoq := Some f let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Nametab.global r) + | RefClass r -> Class.class_of_global (global_with_alias r) (*******************) (* "Show" commands *) @@ -284,8 +285,8 @@ let vernac_bind_scope sc cll = let vernac_open_close_scope = Notation.open_close_scope -let vernac_arguments_scope local qid scl = - Notation.declare_arguments_scope local (global qid) scl +let vernac_arguments_scope local r scl = + Notation.declare_arguments_scope local (global_with_alias r) scl let vernac_infix = Metasyntax.add_infix @@ -506,24 +507,13 @@ let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import -let vernac_canonical locqid = - Recordops.declare_canonical_structure (Nametab.global locqid) - -let locate_reference ref = - let (loc,qid) = qualid_of_reference ref in - try match Nametab.extended_locate qid with - | TrueGlobal ref -> ref - | SyntacticDef kn -> - match Syntax_def.search_syntactic_definition loc kn with - | Rawterm.RRef (_,ref) -> ref - | _ -> raise Not_found - with Not_found -> - error_global_not_found_loc loc qid +let vernac_canonical r = + Recordops.declare_canonical_structure (global_with_alias r) let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - let ref' = locate_reference ref in + let ref' = global_with_alias ref in Class.try_add_new_coercion_with_target ref' stre source target; if_verbose message ((string_of_reference ref) ^ " is now a coercion") @@ -666,11 +656,11 @@ let vernac_hints = Auto.add_hints let vernac_syntactic_definition = Command.syntax_definition -let vernac_declare_implicits local locqid = function +let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (Nametab.global locqid) imps + Impargs.declare_manual_implicits local (global_with_alias r) imps | None -> - Impargs.declare_implicits local (Nametab.global locqid) + Impargs.declare_implicits local (global_with_alias r) let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in @@ -861,8 +851,8 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -let vernac_set_opacity opaq locqid = - match Nametab.global locqid with +let vernac_set_opacity opaq r = + match global_with_alias r with | ConstRef sp -> if opaq then set_opaque_const sp else set_transparent_const sp @@ -962,7 +952,7 @@ let vernac_print = function | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ()) | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ())) | PrintUniverses (Some s) -> dump_universes s - | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid) + | PrintHint r -> Auto.print_hint_ref (global_with_alias r) | PrintHintGoal -> Auto.print_applicable_hint () | PrintHintDbName s -> Auto.print_hint_db_by_name s | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s @@ -977,17 +967,14 @@ let vernac_print = function | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) (*spiwack: prints all the axioms and section variables used by a term *) - | PrintNeededAssumptions qid -> - let cstr = constr_of_reference (global qid) - in - let nassumptions = Environ.needed_assumptions cstr - (Global.env ()) - in + | PrintNeededAssumptions r -> + let cstr = constr_of_global (global_with_alias r) in + let nassumptions = Environ.needed_assumptions cstr (Global.env ()) in msg (try Printer.pr_assumptionset (Global.env ()) nassumptions with Not_found -> - pr_reference qid ++ str " is closed under the global context") + pr_reference r ++ str " is closed under the global context") let global_module r = let (loc,qid) = qualid_of_reference r in @@ -1003,7 +990,7 @@ let interp_search_restriction = function open Search let interp_search_about_item = function - | SearchRef qid -> GlobSearchRef (Nametab.global qid) + | SearchRef r -> GlobSearchRef (global_with_alias r) | SearchString s -> GlobSearchString s let vernac_search s r = @@ -1016,8 +1003,8 @@ let vernac_search s r = | SearchRewrite c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in Search.search_rewrite pat r - | SearchHead locqid -> - Search.search_by_head (Nametab.global locqid) r + | SearchHead ref -> + Search.search_by_head (global_with_alias ref) r | SearchAbout sl -> Search.search_about (List.map interp_search_about_item sl) r diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 67ba2bd52..4a200591e 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -28,6 +28,7 @@ open Command open Pfedit open Refiner open Tacmach +open Syntax_def (* Coq interface to the Whelp query engine developed at the University of Bologna *) @@ -192,13 +193,6 @@ let whelp_locate s = let whelp_elim ind = send_whelp "elim" (make_string uri_of_global (IndRef ind)) -let locate_inductive r = - let (loc,qid) = qualid_of_reference r in - try match Syntax_def.locate_global qid with - | IndRef ind -> ind - | _ -> user_err_loc (loc,"",str "Inductive type expected") - with Not_found -> error_global_not_found_loc loc qid - let on_goal f = let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) @@ -221,7 +215,7 @@ END VERNAC COMMAND EXTEND Whelp | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END -- cgit v1.2.3