From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. --- tactics/btermdn.ml | 2 +- tactics/hints.ml | 42 +++++++++++++++++++++--------------------- tactics/hints.mli | 35 +++++++++++++++++------------------ tactics/hipattern.ml | 6 +++--- tactics/hipattern.mli | 2 +- tactics/tacticals.mli | 4 ++-- tactics/tactics.ml | 2 +- tactics/tactics.mli | 5 ++--- tactics/term_dnet.ml | 2 +- 9 files changed, 49 insertions(+), 51 deletions(-) (limited to 'tactics') diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8e50c977e..8f50b0aa2 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -22,7 +22,7 @@ open Globnames let dnet_depth = ref 8 type term_label = -| GRLabel of global_reference +| GRLabel of GlobRef.t | ProdLabel | LambdaLabel | SortLabel diff --git a/tactics/hints.ml b/tactics/hints.ml index 739f1014a..d02bab186 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -115,7 +115,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen @@ -126,10 +126,10 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { @@ -153,7 +153,7 @@ type 'a with_metadata = { type full_hint = hint with_metadata -type hint_entry = global_reference option * +type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata type import_level = [ `LAX | `WARN | `STRICT ] @@ -308,7 +308,7 @@ let instantiate_hint env sigma p = { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with -| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 +| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2 | PathAny, PathAny -> true | _ -> false @@ -365,7 +365,7 @@ let path_seq p p' = let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with - | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs' + | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs' | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) @@ -474,28 +474,28 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t -val find : global_reference -> t -> search_entry +val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list -val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list +val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_eauto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t -val remove_one : global_reference -> t -> t -val remove_list : global_reference list -> t -> t -val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val remove_one : GlobRef.t -> t -> t +val remove_list : GlobRef.t list -> t -> t +val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t val add_cut : hints_path -> t -> t -val add_mode : global_reference -> hint_mode array -> t -> t +val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path val unfolds : t -> Id.Set.t * Cset.t -val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> +val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a end = @@ -510,7 +510,7 @@ struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list; + hintdb_nopat : (GlobRef.t option * stored_data) list; hintdb_name : string option; } @@ -664,7 +664,7 @@ struct let remove_list grs db = let filter (_, h) = - match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in + match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } @@ -1015,9 +1015,9 @@ type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool | AddHints of hint_entry list - | RemoveHints of global_reference list + | RemoveHints of GlobRef.t list | AddCut of hints_path - | AddMode of global_reference * hint_mode array + | AddMode of GlobRef.t * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -1226,7 +1226,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" diff --git a/tactics/hints.mli b/tactics/hints.mli index b06ede0e1..c7de10a2a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -12,7 +12,6 @@ open Util open Names open EConstr open Environ -open Globnames open Decl_kinds open Evd open Misctypes @@ -25,7 +24,7 @@ open Vernacexpr exception Bound -val decompose_app_bound : evar_map -> constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array type debug = Debug | Info | Off @@ -51,7 +50,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -81,7 +80,7 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool @@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen + Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t - val find : global_reference -> t -> search_entry + val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that @@ -107,27 +106,27 @@ module Hint_db : val map_none : secvars:Id.Pred.t -> t -> full_hint list (** All hints associated to the reference *) - val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t - val remove_one : global_reference -> t -> t - val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> + val remove_one : GlobRef.t -> t -> t + val remove_list : GlobRef.t list -> t -> t + val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool @@ -147,7 +146,7 @@ type hnf = bool type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type hints_entry = @@ -157,7 +156,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit -val remove_hints : bool -> hint_db_name list -> global_reference list -> unit +val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t @@ -264,7 +263,7 @@ val rewrite_db : hint_db_name val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b012a7ecd..b8f1ed720 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -294,13 +294,13 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if eq_gr (IndRef ind) glob_eq then + if GlobRef.equal (IndRef ind) glob_eq then Some (build_coq_eq_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_identity then + else if GlobRef.equal (IndRef ind) glob_identity then Some (build_coq_identity_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_jmeq then + else if GlobRef.equal (IndRef ind) glob_jmeq then Some (build_coq_jmeq_data()),hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 0697d0f19..f04cda123 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index bc2f60186..cbaf691f1 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -135,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) @@ -268,5 +268,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic + val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59c035e83..ee76ad077 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3453,7 +3453,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7809dbf48..46f782eaa 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,7 +16,6 @@ open Proof_type open Evd open Clenv open Redexpr -open Globnames open Pattern open Unification open Misctypes @@ -177,7 +176,7 @@ val change : val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -val unfold_constr : global_reference -> unit Proofview.tactic +val unfold_constr : GlobRef.t -> unit Proofview.tactic (** {6 Modification of the local context. } *) @@ -253,7 +252,7 @@ val apply_delayed_in : type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 753c608ad..611799990 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -37,7 +37,7 @@ struct type 't t = | DRel | DSort - | DRef of global_reference + | DRef of GlobRef.t | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) | DLambda of 't * 't | DApp of 't * 't (* binary app *) -- cgit v1.2.3