From 159439ffffa12831e09206a8b70362fae53a3111 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 27 Dec 2024 16:21:34 +0100 Subject: [PATCH] explicit export locality for Hint commands in all generated Coq code --- src/grammar_pp.ml | 2 +- src/ln_transform.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 85ffd57..1b7f633 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -1250,7 +1250,7 @@ and coq_maybe_decide_equality m xd homs ntmvr loc = | [ Hom_string s ] -> s | _ -> Auxl.error (Some loc) "malformed coq-equality homomorphism\n" ) ^ "\nDefined.\n" - ^ "Hint Resolve eq_" ^ type_name ^ " : ott_coq_equality.\n" + ^ "#[export] Hint Resolve eq_" ^ type_name ^ " : ott_coq_equality.\n" and pp_metavardefn m xd mvd = let pp_com = pp_com_strings m xd mvd.mvd_rep [pp_metavar_with_sie m xd [] (mvd.mvd_name,[])] in diff --git a/src/ln_transform.ml b/src/ln_transform.ml index 570e1f1..f11be18 100644 --- a/src/ln_transform.ml +++ b/src/ln_transform.ml @@ -1758,7 +1758,7 @@ Tactic Notation \"apply_fresh\" \"*\" constr(T) \"as\" ident(x) := let h = hints_rel @ hints_lc in if List.length h = 0 then "" - else "Hint Constructors "^(String.concat " " h)^" : core.\n" in + else "#[export] Hint Constructors "^(String.concat " " h)^" : core.\n" in (* ** all together *) "\n(** infrastructure *)\n"