diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 46d162911..3ade5314b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -28,12 +28,13 @@ open Termops open Inductiveops open Typing open Decl_kinds +open Vernacexpr +open Typeclasses open Pattern open Patternops open Clenv open Tacred open Printer -open Vernacexpr module NamedDecl = Context.Named.Declaration @@ -94,7 +95,6 @@ let secvars_of_hyps hyps = else pred let empty_hint_info = - let open Vernacexpr in { hint_priority = None; hint_pattern = None } (************************************************************************) @@ -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) @@ -448,7 +448,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -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; } @@ -654,7 +654,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.smartfilter p sdl + let remove_sdl p sdl = List.Smart.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -664,9 +664,9 @@ 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 + let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with | IsGlobRef gr -> - let (c, ctx) = Universes.fresh_global_instance env gr in + let (c, ctx) = UnivGen.fresh_global_instance env gr in true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in @@ -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 @@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> @@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path 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" |