aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/dp/dp.ml4
-rw-r--r--contrib/funind/indfun_common.ml2
-rw-r--r--contrib/recdef/recdef.ml436
-rw-r--r--contrib/setoid_ring/newring.ml46
-rw-r--r--contrib/subtac/subtac_command.ml4
-rw-r--r--interp/syntax_def.ml18
-rw-r--r--interp/syntax_def.mli17
-rw-r--r--library/libnames.ml2
-rw-r--r--library/libnames.mli2
-rw-r--r--library/nametab.ml4
-rwxr-xr-xlibrary/nametab.mli4
-rw-r--r--pretyping/classops.ml6
-rw-r--r--pretyping/detyping.ml11
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--tactics/auto.ml10
-rw-r--r--tactics/decl_interp.ml2
-rw-r--r--tactics/decl_proof_instr.ml2
-rw-r--r--tactics/tacinterp.ml16
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/vernacentries.ml53
-rw-r--r--toplevel/whelp.ml410
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:46:59 +0000