From 4ebccb9d2722a7323cb7fce5c9e00bf2eea5b69f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Jun 2020 12:59:06 +0200 Subject: Dnets now consider axioms as being opaque for pattern recognition. --- tactics/auto.ml | 28 ++++++++++---------- tactics/btermdn.ml | 67 ++++++++++++++++++++++++++++++------------------ tactics/btermdn.mli | 4 +-- tactics/class_tactics.ml | 6 ++--- tactics/eauto.ml | 6 ++--- tactics/hints.ml | 43 ++++++++++++++++--------------- tactics/hints.mli | 8 +++--- 7 files changed, 91 insertions(+), 71 deletions(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index 488bcb5208..784322679f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -266,7 +266,7 @@ let flags_of_state st = let auto_flags_of_state st = auto_unif_flags_of TransparentState.full st -let hintmap_of sigma secvars hdc concl = +let hintmap_of env sigma secvars hdc concl = match hdc with | None -> Hint_db.map_none ~secvars | Some hdc -> @@ -274,7 +274,7 @@ let hintmap_of sigma secvars hdc concl = (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with | ModeMatch l -> l | ModeMismatch -> []) - else Hint_db.map_auto sigma ~secvars hdc concl + else Hint_db.map_auto env sigma ~secvars hdc concl let exists_evaluable_reference env = function | EvalConstRef _ -> true @@ -300,23 +300,24 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = Proofview.Goal.enter begin fun gl -> let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in + let env = Proofview.Goal.env gl in let secvars = compute_secvars gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE - (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl))) + (trivial_resolve env sigma dbg mod_delta db_list local_db secvars concl))) end -and my_find_search_nodelta sigma db_list local_db secvars hdc concl = +and my_find_search_nodelta env sigma db_list local_db secvars hdc concl = List.map (fun hint -> (None,hint)) - (List.map_append (hintmap_of sigma secvars hdc concl) (local_db::db_list)) + (List.map_append (hintmap_of env sigma secvars hdc concl) (local_db::db_list)) and my_find_search mod_delta = if mod_delta then my_find_search_delta else my_find_search_nodelta -and my_find_search_delta sigma db_list local_db secvars hdc concl = - let f = hintmap_of sigma secvars hdc concl in +and my_find_search_delta env sigma db_list local_db secvars hdc concl = + let f = hintmap_of env sigma secvars hdc concl in if occur_existential sigma concl then List.map_append (fun db -> @@ -340,7 +341,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = | None -> Hint_db.map_none ~secvars db | Some hdc -> if TransparentState.is_empty st - then Hint_db.map_auto sigma ~secvars hdc concl db + then Hint_db.map_auto env sigma ~secvars hdc concl db else match Hint_db.map_existential sigma ~secvars hdc concl db with | ModeMatch l -> l | ModeMismatch -> [] @@ -381,7 +382,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) = in tclLOG dbg pr_hint (FullHint.run h tactic) -and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = +and trivial_resolve env sigma dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound sigma cl in @@ -390,7 +391,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = in List.map (tac_of_hint dbg db_list local_db cl) (priority - (my_find_search mod_delta sigma db_list local_db secvars head cl)) + (my_find_search mod_delta env sigma db_list local_db secvars head cl)) with Not_found -> [] (** The use of the "core" database can be de-activated by passing @@ -430,7 +431,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l (* The classical Auto tactic *) (**************************************************************************) -let possible_resolve sigma dbg mod_delta db_list local_db secvars cl = +let possible_resolve env sigma dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound sigma cl in @@ -438,7 +439,7 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl = with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (my_find_search mod_delta sigma db_list local_db secvars head cl) + (my_find_search mod_delta env sigma db_list local_db secvars head cl) with Not_found -> [] let extend_local_db decl db gl = @@ -473,12 +474,13 @@ let search d n mod_delta db_list local_db = ( Proofview.Goal.enter begin fun gl -> let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in + let env = Proofview.Goal.env gl in let secvars = compute_secvars gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve sigma d mod_delta db_list local_db secvars concl)) + (possible_resolve env sigma d mod_delta db_list local_db secvars concl)) end)) end [] in diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 1f148e01fa..bacb5a7b8f 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -49,17 +49,25 @@ let decomp sigma t = in decrec [] t -let constr_val_discr sigma t = +let evaluable_constant c env = + (* This is a hack to work around a broken Print Module implementation, see + bug #2668. *) + if Environ.mem_constant c env then Environ.evaluable_constant c env + else true + +let constr_val_discr env sigma t = let open GlobRef in let c, l = decomp sigma t in match EConstr.kind sigma c with | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) | Var id -> Label(GRLabel (VarRef id),l) - | Const _ -> Everything + | Const (c, _) -> + if evaluable_constant c env then Everything + else Label(GRLabel (ConstRef c),l) | _ -> Nothing -let constr_pat_discr t = +let constr_pat_discr env t = if not (Patternops.occur_meta_pattern t) then None else @@ -68,16 +76,23 @@ let constr_pat_discr t = | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args) + | PRef ((ConstRef c) as ref), args -> + if evaluable_constant c env then None + else Some (GRLabel ref, args) | _ -> None -let constr_val_discr_st sigma ts t = +let constr_val_discr_st env sigma ts t = let c, l = decomp sigma t in let open GlobRef in match EConstr.kind sigma c with - | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) + | Const (c,u) -> + if evaluable_constant c env && TransparentState.is_transparent_constant ts c then Everything + else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l) + | Var id -> + if Environ.evaluable_named id env && TransparentState.is_transparent_variable ts id then Everything + else Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> if List.is_empty l then @@ -88,52 +103,54 @@ let constr_val_discr_st sigma ts t = | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _ | Proj _ | Int _ | Float _ | Array _ -> Nothing -let constr_pat_discr_st ts t = +let constr_pat_discr_st env ts t = let open GlobRef in match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) -> - Some(GRLabel ref,args) + | PRef ((VarRef v) as ref), args -> + if Environ.evaluable_named v env && (TransparentState.is_transparent_variable ts v) then None + else Some(GRLabel ref,args) + | PRef ((ConstRef c) as ref), args -> + if evaluable_constant c env && TransparentState.is_transparent_constant ts c then None + else Some (GRLabel ref, args) | PVar v, args when not (TransparentState.is_transparent_variable ts v) -> Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) -> - Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) | PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c]) | PSort s, [] -> Some (SortLabel, []) | _ -> None -let bounded_constr_pat_discr_st st (t,depth) = +let bounded_constr_pat_discr_st env st (t,depth) = if Int.equal depth 0 then None else - match constr_pat_discr_st st t with + match constr_pat_discr_st env st t with | None -> None | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) -let bounded_constr_val_discr_st sigma st (t,depth) = +let bounded_constr_val_discr_st env sigma st (t,depth) = if Int.equal depth 0 then Nothing else - match constr_val_discr_st sigma st t with + match constr_val_discr_st env sigma st t with | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) | Nothing -> Nothing | Everything -> Everything -let bounded_constr_pat_discr (t,depth) = +let bounded_constr_pat_discr env (t,depth) = if Int.equal depth 0 then None else - match constr_pat_discr t with + match constr_pat_discr env t with | None -> None | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) -let bounded_constr_val_discr sigma (t,depth) = +let bounded_constr_val_discr env sigma (t,depth) = if Int.equal depth 0 then Nothing else - match constr_val_discr sigma t with + match constr_val_discr env sigma t with | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) | Nothing -> Nothing | Everything -> Everything @@ -153,21 +170,21 @@ struct type pattern = Dn.pattern - let pattern st pat = match st with - | None -> Dn.pattern bounded_constr_pat_discr (pat, !dnet_depth) - | Some st -> Dn.pattern (bounded_constr_pat_discr_st st) (pat, !dnet_depth) + let pattern env st pat = match st with + | None -> Dn.pattern (bounded_constr_pat_discr env) (pat, !dnet_depth) + | Some st -> Dn.pattern (bounded_constr_pat_discr_st env st) (pat, !dnet_depth) let empty = Dn.empty let add = Dn.add let rmv = Dn.rmv - let lookup sigma = function + let lookup env sigma = function | None -> (fun dn t -> - Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth)) + Dn.lookup dn (bounded_constr_val_discr env sigma) (t,!dnet_depth)) | Some st -> (fun dn t -> - Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth)) + Dn.lookup dn (bounded_constr_val_discr_st env sigma st) (t,!dnet_depth)) let app f dn = Dn.app f dn diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 2caa193202..ab201a1872 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -30,14 +30,14 @@ sig type pattern - val pattern : TransparentState.t option -> constr_pattern -> pattern + val pattern : Environ.env -> TransparentState.t option -> constr_pattern -> pattern val empty : t val add : t -> pattern -> Z.t -> t val rmv : t -> pattern -> Z.t -> t - val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list + val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list val app : (Z.t -> unit) -> t -> unit end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 378a3e718b..2f55cc071f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -257,13 +257,13 @@ let shelve_dependencies gls = Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls); shelve_goals gls) -let hintmap_of sigma hdc secvars concl = +let hintmap_of env sigma hdc secvars concl = match hdc with | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db) | Some hdc -> fun db -> if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma ~secvars hdc concl db + Hint_db.map_eauto env sigma ~secvars hdc concl db else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) @@ -373,7 +373,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp)) | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp)) in - let hint_of_db = hintmap_of sigma hdc secvars concl in + let hint_of_db = hintmap_of env sigma hdc secvars concl in let hintl = List.map_filter (fun db -> match hint_of_db db with | ModeMatch l -> Some (db, l) | ModeMismatch -> None) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 17e6a6edb4..e920093648 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -67,7 +67,7 @@ open Auto let unify_e_resolve flags h = Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h -let hintmap_of sigma secvars concl = +let hintmap_of env sigma secvars concl = (* Warning: for computation sharing, we need to return a closure *) let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in match hdc with @@ -78,7 +78,7 @@ let hintmap_of sigma secvars concl = match Hint_db.map_existential sigma ~secvars hdc concl db with | ModeMatch l -> l | ModeMismatch -> []) - else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) + else (fun db -> Hint_db.map_auto env sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact flags h = @@ -106,7 +106,7 @@ let rec e_trivial_fail_db db_list local_db = end and e_my_find_search env sigma db_list local_db secvars concl = - let hint_of_db = hintmap_of sigma secvars concl in + let hint_of_db = hintmap_of env sigma secvars concl in let hintl = List.map_append (fun db -> let flags = auto_flags_of_state (Hint_db.transparent_state db) in diff --git a/tactics/hints.ml b/tactics/hints.ml index 4532f97a27..7d065df19b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -243,7 +243,7 @@ sig type t val empty : t val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t - val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list + val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list end = struct module Data = struct type t = stored_data let compare = pri_order_int end @@ -257,18 +257,18 @@ struct let add st net p v = ref (Diff ((st, p, v), net)) - let rec force net = match !net with + let rec force env net = match !net with | Bnet dn -> dn | Diff ((st, p, v), rem) -> - let dn = force rem in - let p = Bnet.pattern st p in + let dn = force env rem in + let p = Bnet.pattern env st p in let dn = Bnet.add dn p v in let () = net := (Bnet dn) in dn - let lookup sigma st net p = - let dn = force net in - Bnet.lookup sigma st dn p + let lookup env sigma st net p = + let dn = force env net in + Bnet.lookup env sigma st dn p end type search_entry = { @@ -307,8 +307,8 @@ let rebuild_dn st se = in { se with sentry_bnet = dn' } -let lookup_tacs sigma concl st se = - let l' = Bounded_net.lookup sigma st se.sentry_bnet concl in +let lookup_tacs env sigma concl st se = + let l' = Bounded_net.lookup env sigma st se.sentry_bnet concl in let sl' = List.stable_sort pri_order_int l' in List.merge pri_order_int se.sentry_nopat sl' @@ -529,14 +529,14 @@ val map_none : secvars:Id.Pred.t -> 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 -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode -val map_eauto : evar_map -> secvars:Id.Pred.t -> +val map_eauto : Environ.env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode -val map_auto : evar_map -> secvars:Id.Pred.t -> +val map_auto : Environ.env -> evar_map -> secvars:Id.Pred.t -> (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 : GlobRef.t -> t -> t -val remove_list : GlobRef.t list -> t -> t +val remove_one : Environ.env -> GlobRef.t -> t -> t +val remove_list : Environ.env -> 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 -> TransparentState.t @@ -629,10 +629,10 @@ struct merge_entry secvars db se.sentry_nopat se.sentry_pat (* Precondition: concl has no existentials *) - let map_auto sigma ~secvars (k,args) concl db = + let map_auto env sigma ~secvars (k,args) concl db = let se = find k db in let st = if db.use_dn then (Some db.hintdb_state) else None in - let pat = lookup_tacs sigma concl st se in + let pat = lookup_tacs env sigma concl st se in merge_entry secvars db [] pat let map_existential sigma ~secvars (k,args) concl db = @@ -642,11 +642,11 @@ struct else ModeMismatch (* [c] contains an existential *) - let map_eauto sigma ~secvars (k,args) concl db = + let map_eauto env sigma ~secvars (k,args) concl db = let se = find k db in if matches_modes sigma args se.sentry_mode then let st = if db.use_dn then Some db.hintdb_state else None in - let pat = lookup_tacs sigma concl st se in + let pat = lookup_tacs env sigma concl st se in ModeMatch (merge_entry secvars db [] pat) else ModeMismatch @@ -720,14 +720,14 @@ struct if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' } - let remove_list grs db = + let remove_list env grs db = let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map in let hintnopat = List.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 + let remove_one env gr db = remove_list env [gr] db let get_entry se = let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in @@ -1044,8 +1044,9 @@ let add_transparency dbname target b = in searchtable_add (dbname, Hint_db.set_transparent_state db st') let remove_hint dbname grs = + let env = Global.env () in let db = get_db dbname in - let db' = Hint_db.remove_list grs db in + let db' = Hint_db.remove_list env grs db in searchtable_add (dbname, db') type hint_action = @@ -1463,7 +1464,7 @@ let pr_hint_term env sigma cl = (fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with | ModeMatch l -> l | ModeMismatch -> []) - else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl + else Hint_db.map_auto env sigma ~secvars:Id.Pred.full hdc cl with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in let fn db = List.map (fun x -> 0, x) (fn db) in diff --git a/tactics/hints.mli b/tactics/hints.mli index 0b9da27ab3..e061bd7648 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -134,18 +134,18 @@ module Hint_db : (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. Returns a [ModeMismatch] if there are declared modes and none matches. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode + val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode (** All hints associated to the reference. Precondition: no evars should appear in the arguments, so no modes are checked. *) - val map_auto : evar_map -> secvars:Id.Pred.t -> + val map_auto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t 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 : GlobRef.t -> t -> t - val remove_list : GlobRef.t list -> t -> t + val remove_one : Environ.env -> GlobRef.t -> t -> t + val remove_list : Environ.env -> GlobRef.t list -> t -> t val iter : (GlobRef.t option -> hint_mode array list -> FullHint.t list -> unit) -> t -> unit -- cgit v1.2.3 From ca58a8015646158fae415ef4b3edc350d6eaefbc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Aug 2020 17:33:30 +0200 Subject: Do not store the transparent state in delayed dnets. We know statically that it is going to be the one provided at the time of lookup, so we simply fetch it from there. --- tactics/hints.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tactics/hints.ml b/tactics/hints.ml index 7d065df19b..db4b23705f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -249,25 +249,25 @@ struct module Data = struct type t = stored_data let compare = pri_order_int end module Bnet = Btermdn.Make(Data) - type diff = TransparentState.t option * Pattern.constr_pattern * stored_data + type diff = Pattern.constr_pattern * stored_data type data = Bnet of Bnet.t | Diff of diff * data ref type t = data ref let empty = ref (Bnet Bnet.empty) - let add st net p v = ref (Diff ((st, p, v), net)) + let add _st net p v = ref (Diff ((p, v), net)) - let rec force env net = match !net with + let rec force env st net = match !net with | Bnet dn -> dn - | Diff ((st, p, v), rem) -> - let dn = force env rem in + | Diff ((p, v), rem) -> + let dn = force env st rem in let p = Bnet.pattern env st p in let dn = Bnet.add dn p v in let () = net := (Bnet dn) in dn let lookup env sigma st net p = - let dn = force env net in + let dn = force env st net in Bnet.lookup env sigma st dn p end -- cgit v1.2.3 From 94bbe5b1d05f72d63eb72a407673a18df16fd7ed Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Aug 2020 15:14:23 +0200 Subject: Adding overlays. --- dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh diff --git a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh new file mode 100644 index 0000000000..7c04608403 --- /dev/null +++ b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12565" ] || [ "$CI_BRANCH" = "fix-tc-search-opacity" ]; then + + coqhammer_CI_REF=fix-tc-search-opacity + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi -- cgit v1.2.3