Commit fc82b6c8 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Qualify `Hint` as `Global Hint` where appropriate

This avoids a new warning of Coq 8.13.

Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
parent eca14936
......@@ -17,7 +17,7 @@ Require Import Alphabet.
Class IsValidator (P : Prop) (b : bool) :=
is_validator : b = true -> P.
Hint Mode IsValidator + - : typeclass_instances.
Global Hint Mode IsValidator + - : typeclass_instances.
Instance is_validator_true : IsValidator True true.
Proof. done. Qed.
......@@ -55,12 +55,12 @@ Qed.
(* We do not use an instance directly here, because we need somehow to
force Coq to instantiate b with a lambda. *)
Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
Global Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
: typeclass_instances.
(* Hint for synthetizing pattern-matching. *)
Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
Global Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
let b := fresh "b" in
unshelve notypeclasses refine (let b : bool := _ in _);
[destruct u; intros; shelve|]; (* Synthetize `match .. with` in the validator. *)
......@@ -71,5 +71,5 @@ Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
(* Hint for unfolding definitions. This is necessary because many
hints for IsValidator use [Hint Extern], which do not automatically
unfold identifiers. *)
Hint Extern 100 (IsValidator ?X _) => unfold X
Global Hint Extern 100 (IsValidator ?X _) => unfold X
: typeclass_instances.
......@@ -140,7 +140,7 @@ Qed.
(* We do not declare this lemma as an instance, and use [Hint Extern]
instead, because the typeclass mechanism has trouble instantiating
some evars if we do not explicitely call [eassumption]. *)
Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
Global Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
eapply is_validator_state_has_future_subset; [eassumption|eassumption || reflexivity|]
: typeclass_instances.
......@@ -171,7 +171,7 @@ Proof.
- destruct (b lookahead). by destruct b'. exfalso. by induction l; destruct b'.
- eauto.
Qed.
Hint Extern 100 (IsValidator _ _) =>
Global Hint Extern 100 (IsValidator _ _) =>
match goal with
| H : TerminalSet.In ?lookahead ?lset |- _ =>
eapply (is_validator_iterate_lset _ (fun lookahead => _) _ _ H); clear H
......@@ -238,7 +238,7 @@ Proof.
revert EQ. unfold future_of_prod=>-> //.
Qed.
(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *)
Hint Extern 0 (IsValidator
Global Hint Extern 0 (IsValidator
(forall st prod fut lookahead,
state_has_future st prod fut lookahead -> _)
_) =>
......
......@@ -26,7 +26,7 @@ Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC.
Proof.
destruct r; simpl; congruence.
Qed.
Hint Resolve preg_of_iregsp_not_PC: asmgen.
Global Hint Resolve preg_of_iregsp_not_PC: asmgen.
Lemma preg_of_not_X16: forall r, preg_of r <> X16.
Proof.
......@@ -44,7 +44,7 @@ Proof.
intros. apply ireg_of_not_X16 in H. congruence.
Qed.
Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
Global Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen.
(** Useful simplification tactic *)
......
......@@ -335,7 +335,7 @@ Proof.
eapply loc_arguments_rec_charact; eauto. lia.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
Global Hint Resolve loc_arguments_acceptable: locs.
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
......
......@@ -40,14 +40,14 @@ Lemma ireg_of_not_R14:
Proof.
intros. erewrite <- ireg_of_eq; eauto with asmgen.
Qed.
Hint Resolve ireg_of_not_R14: asmgen.
Global Hint Resolve ireg_of_not_R14: asmgen.
Lemma ireg_of_not_R14':
forall m r, ireg_of m = OK r -> r <> IR14.
Proof.
intros. generalize (ireg_of_not_R14 _ _ H). congruence.
Qed.
Hint Resolve ireg_of_not_R14': asmgen.
Global Hint Resolve ireg_of_not_R14': asmgen.
(** [undef_flags] and [nextinstr_nf] *)
......@@ -75,7 +75,7 @@ Proof.
intros; red; intros; subst; discriminate.
Qed.
Hint Resolve data_if_preg if_preg_not_PC: asmgen.
Global Hint Resolve data_if_preg if_preg_not_PC: asmgen.
Lemma nextinstr_nf_inv:
forall r rs, if_preg r = true -> (nextinstr_nf rs)#r = rs#r.
......
......@@ -427,7 +427,7 @@ Proof.
destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
Global Hint Resolve loc_arguments_acceptable: locs.
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
......
......@@ -31,7 +31,7 @@ Require Import Conventions.
(** * Processor registers and register states *)
Hint Extern 2 (_ <> _) => congruence: asmgen.
Global Hint Extern 2 (_ <> _) => congruence: asmgen.
Lemma ireg_of_eq:
forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
......@@ -56,7 +56,7 @@ Lemma preg_of_data:
Proof.
intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data: asmgen.
Global Hint Resolve preg_of_data: asmgen.
Lemma data_diff:
forall r r',
......@@ -64,7 +64,7 @@ Lemma data_diff:
Proof.
congruence.
Qed.
Hint Resolve data_diff: asmgen.
Global Hint Resolve data_diff: asmgen.
Lemma preg_of_not_SP:
forall r, preg_of r <> SP.
......@@ -78,7 +78,7 @@ Proof.
intros. apply data_diff; auto with asmgen.
Qed.
Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
Global Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
Lemma nextinstr_pc:
forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one.
......@@ -746,7 +746,7 @@ Qed.
Definition nolabel (i: instruction) :=
match i with Plabel _ => False | _ => True end.
Hint Extern 1 (nolabel _) => exact I : labels.
Global Hint Extern 1 (nolabel _) => exact I : labels.
Lemma tail_nolabel_cons:
forall i c k,
......@@ -757,7 +757,7 @@ Proof.
intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
Qed.
Hint Resolve tail_nolabel_refl: labels.
Global Hint Resolve tail_nolabel_refl: labels.
Ltac TailNoLabel :=
eauto with labels;
......
......@@ -92,7 +92,7 @@ Record wf_numbering (n: numbering) : Prop := {
In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
}.
Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
(** Satisfiability of numberings. A numbering holds in a concrete
execution state if there exists a valuation assigning values to
......@@ -130,7 +130,7 @@ Record numbering_holds (valu: valuation) (ge: genv) (sp: val)
n.(num_reg)!r = Some v -> rs#r = valu v
}.
Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
Global Hint Resolve num_holds_wf num_holds_eq num_holds_reg: cse.
Lemma empty_numbering_holds:
forall valu ge sp rs m,
......
......@@ -464,7 +464,7 @@ Inductive final_state: state -> int -> Prop :=
Definition semantics (p: program) :=
Semantics step (initial_state p) final_state (Genv.globalenv p).
Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
(** * Lifting of let-bound variables *)
......@@ -580,4 +580,4 @@ Proof.
eexact H. apply insert_lenv_0.
Qed.
Hint Resolve eval_lift: evalexpr.
Global Hint Resolve eval_lift: evalexpr.
......@@ -290,7 +290,7 @@ Lemma expect_incr: forall te e t1 t2 e',
Proof.
unfold expect; intros. destruct (typ_eq t1 t2); inv H; auto.
Qed.
Hint Resolve expect_incr: ty.
Global Hint Resolve expect_incr: ty.
Lemma expect_sound: forall e t1 t2 e',
expect e t1 t2 = OK e' -> t1 = t2.
......@@ -305,7 +305,7 @@ Proof.
- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
Qed.
Hint Resolve type_expr_incr: ty.
Global Hint Resolve type_expr_incr: ty.
Lemma type_expr_sound: forall te a t e e',
type_expr e a t = OK e' -> S.satisf te e' -> wt_expr te a t.
......@@ -325,7 +325,7 @@ Lemma type_exprlist_incr: forall te al tl e e',
Proof.
induction al; destruct tl; simpl; intros until e'; intros T SAT; monadInv T; eauto with ty.
Qed.
Hint Resolve type_exprlist_incr: ty.
Global Hint Resolve type_exprlist_incr: ty.
Lemma type_exprlist_sound: forall te al tl e e',
type_exprlist e al tl = OK e' -> S.satisf te e' -> list_forall2 (wt_expr te) al tl.
......@@ -342,7 +342,7 @@ Proof.
- destruct (type_unop u) as [targ1 tres]; monadInv T; eauto with ty.
- destruct (type_binop b) as [[targ1 targ2] tres]; monadInv T; eauto with ty.
Qed.
Hint Resolve type_assign_incr: ty.
Global Hint Resolve type_assign_incr: ty.
Lemma type_assign_sound: forall te id a e e',
type_assign e id a = OK e' -> S.satisf te e' -> wt_expr te a (te id).
......@@ -362,7 +362,7 @@ Lemma opt_set_incr: forall te optid optty e e',
Proof.
unfold opt_set; intros. destruct optid, optty; try (monadInv H); eauto with ty.
Qed.
Hint Resolve opt_set_incr: ty.
Global Hint Resolve opt_set_incr: ty.
Lemma opt_set_sound: forall te optid sg e e',
opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' ->
......@@ -379,7 +379,7 @@ Proof.
induction s; simpl; intros e1 e2 T SAT; try (monadInv T); eauto with ty.
- destruct tret, o; try (monadInv T); eauto with ty.
Qed.
Hint Resolve type_stmt_incr: ty.
Global Hint Resolve type_stmt_incr: ty.
Lemma type_stmt_sound: forall te tret s e e',
type_stmt tret e s = OK e' -> S.satisf te e' -> wt_stmt te tret s.
......
......@@ -358,7 +358,7 @@ Proof.
intros. destruct ros; simpl in *. eapply add_need_all_eagree; eauto. auto.
Qed.
Hint Resolve add_need_all_eagree add_need_all_lessdef
Global Hint Resolve add_need_all_eagree add_need_all_lessdef
add_need_eagree add_need_vagree
add_needs_all_eagree add_needs_all_lessdef
add_needs_eagree add_needs_vagree
......
......@@ -74,7 +74,7 @@ Proof.
intros. simpl in H. auto.
Qed.
Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
Inductive vagree_list: list val -> list val -> list nval -> Prop :=
| vagree_list_nil: forall nvl,
......@@ -100,7 +100,7 @@ Proof.
destruct nvl; constructor; auto with na.
Qed.
Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
Global Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.
(** ** Ordering and least upper bound between value needs *)
......@@ -116,8 +116,8 @@ Proof.
destruct x; constructor; auto.
Qed.
Hint Constructors nge: na.
Hint Resolve nge_refl: na.
Global Hint Constructors nge: na.
Global Hint Resolve nge_refl: na.
Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z.
Proof.
......@@ -1084,7 +1084,7 @@ Proof.
intros. apply H.
Qed.
Hint Resolve nreg_agree: na.
Global Hint Resolve nreg_agree: na.
Lemma eagree_ge:
forall e1 e2 ne ne',
......
......@@ -165,7 +165,7 @@ Proof.
subst r0; contradiction.
apply Regmap.gso; auto.
Qed.
Hint Resolve match_env_update_temp: rtlg.
Global Hint Resolve match_env_update_temp: rtlg.
(** Matching between environments is preserved by simultaneous
assignment to a Cminor local variable (in the Cminor environments)
......@@ -205,7 +205,7 @@ Proof.
eapply match_env_update_temp; eauto.
eapply match_env_update_var; eauto.
Qed.
Hint Resolve match_env_update_dest: rtlg.
Global Hint Resolve match_env_update_dest: rtlg.
(** A variant of [match_env_update_var] corresponding to the assignment
of the result of a builtin. *)
......
......@@ -128,7 +128,7 @@ Ltac monadInv H :=
(** * Monotonicity properties of the state *)
Hint Resolve state_incr_refl: rtlg.
Global Hint Resolve state_incr_refl: rtlg.
Lemma instr_at_incr:
forall s1 s2 n i,
......@@ -137,7 +137,7 @@ Proof.
intros. inv H.
destruct (H3 n); congruence.
Qed.
Hint Resolve instr_at_incr: rtlg.
Global Hint Resolve instr_at_incr: rtlg.
(** The following tactic saturates the hypotheses with
[state_incr] properties that follow by transitivity from
......@@ -174,14 +174,14 @@ Lemma valid_fresh_absurd:
Proof.
intros r s. unfold reg_valid, reg_fresh; case r; tauto.
Qed.
Hint Resolve valid_fresh_absurd: rtlg.
Global Hint Resolve valid_fresh_absurd: rtlg.
Lemma valid_fresh_different:
forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2.
Proof.
unfold not; intros. subst r2. eauto with rtlg.
Qed.
Hint Resolve valid_fresh_different: rtlg.
Global Hint Resolve valid_fresh_different: rtlg.
Lemma reg_valid_incr:
forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2.
......@@ -190,7 +190,7 @@ Proof.
inversion INCR.
unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto.
Qed.
Hint Resolve reg_valid_incr: rtlg.
Global Hint Resolve reg_valid_incr: rtlg.
Lemma reg_fresh_decr:
forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1.
......@@ -199,7 +199,7 @@ Proof.
unfold reg_fresh; unfold not; intros.
apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto.
Qed.
Hint Resolve reg_fresh_decr: rtlg.
Global Hint Resolve reg_fresh_decr: rtlg.
(** Validity of a list of registers. *)
......@@ -211,7 +211,7 @@ Lemma regs_valid_nil:
Proof.
intros; red; intros. elim H.
Qed.
Hint Resolve regs_valid_nil: rtlg.
Global Hint Resolve regs_valid_nil: rtlg.
Lemma regs_valid_cons:
forall r1 rl s,
......@@ -232,7 +232,7 @@ Lemma regs_valid_incr:
Proof.
unfold regs_valid; intros; eauto with rtlg.
Qed.
Hint Resolve regs_valid_incr: rtlg.
Global Hint Resolve regs_valid_incr: rtlg.
(** A register is ``in'' a mapping if it is associated with a Cminor
local or let-bound variable. *)
......@@ -253,7 +253,7 @@ Lemma map_valid_incr:
Proof.
unfold map_valid; intros; eauto with rtlg.
Qed.
Hint Resolve map_valid_incr: rtlg.
Global Hint Resolve map_valid_incr: rtlg.
(** * Properties of basic operations over the state *)
......@@ -265,7 +265,7 @@ Lemma add_instr_at:
Proof.
intros. monadInv H. simpl. apply PTree.gss.
Qed.
Hint Resolve add_instr_at: rtlg.
Global Hint Resolve add_instr_at: rtlg.
(** Properties of [update_instr]. *)
......@@ -278,7 +278,7 @@ Proof.
destruct (check_empty_node s1 n); try discriminate.
inv H. simpl. apply PTree.gss.
Qed.
Hint Resolve update_instr_at: rtlg.
Global Hint Resolve update_instr_at: rtlg.
(** Properties of [new_reg]. *)
......@@ -289,7 +289,7 @@ Proof.
intros. monadInv H.
unfold reg_valid; simpl. apply Plt_succ.
Qed.
Hint Resolve new_reg_valid: rtlg.
Global Hint Resolve new_reg_valid: rtlg.
Lemma new_reg_fresh:
forall s1 s2 r i,
......@@ -299,7 +299,7 @@ Proof.
unfold reg_fresh; simpl.
exact (Plt_strict _).
Qed.
Hint Resolve new_reg_fresh: rtlg.
Global Hint Resolve new_reg_fresh: rtlg.
Lemma new_reg_not_in_map:
forall s1 s2 m r i,
......@@ -307,7 +307,7 @@ Lemma new_reg_not_in_map:
Proof.
unfold not; intros; eauto with rtlg.
Qed.
Hint Resolve new_reg_not_in_map: rtlg.
Global Hint Resolve new_reg_not_in_map: rtlg.
(** * Properties of operations over compilation environments *)
......@@ -330,7 +330,7 @@ Proof.
intros. inv H0. left; exists name; auto.
intros. inv H0.
Qed.
Hint Resolve find_var_in_map: rtlg.
Global Hint Resolve find_var_in_map: rtlg.
Lemma find_var_valid:
forall s1 s2 map name r i,
......@@ -338,7 +338,7 @@ Lemma find_var_valid:
Proof.
eauto with rtlg.
Qed.
Hint Resolve find_var_valid: rtlg.
Global Hint Resolve find_var_valid: rtlg.
(** Properties of [find_letvar]. *)
......@@ -350,7 +350,7 @@ Proof.
caseEq (nth_error (map_letvars map) idx); intros; monadInv H0.
right; apply nth_error_in with idx; auto.
Qed.
Hint Resolve find_letvar_in_map: rtlg.
Global Hint Resolve find_letvar_in_map: rtlg.
Lemma find_letvar_valid:
forall s1 s2 map idx r i,
......@@ -358,7 +358,7 @@ Lemma find_letvar_valid:
Proof.
eauto with rtlg.
Qed.
Hint Resolve find_letvar_valid: rtlg.
Global Hint Resolve find_letvar_valid: rtlg.
(** Properties of [add_var]. *)
......@@ -445,7 +445,7 @@ Proof.
intros until r. unfold alloc_reg.
case a; eauto with rtlg.
Qed.
Hint Resolve alloc_reg_valid: rtlg.
Global Hint Resolve alloc_reg_valid: rtlg.
Lemma alloc_reg_fresh_or_in_map:
forall map a s r s' i,
......@@ -469,7 +469,7 @@ Proof.
apply regs_valid_nil.
apply regs_valid_cons. eauto with rtlg. eauto with rtlg.
Qed.
Hint Resolve alloc_regs_valid: rtlg.
Global Hint Resolve alloc_regs_valid: rtlg.
Lemma alloc_regs_fresh_or_in_map:
forall map al s rl s' i,
......@@ -494,7 +494,7 @@ Proof.
intros until r. unfold alloc_reg.
case dest; eauto with rtlg.
Qed.
Hint Resolve alloc_optreg_valid: rtlg.
Global Hint Resolve alloc_optreg_valid: rtlg.
Lemma alloc_optreg_fresh_or_in_map:
forall map dest s r s' i,
......@@ -609,7 +609,7 @@ Proof.
apply regs_valid_cons; eauto with rtlg.
Qed.
Hint Resolve new_reg_target_ok alloc_reg_target_ok
Global Hint Resolve new_reg_target_ok alloc_reg_target_ok
alloc_regs_target_ok: rtlg.
(** The following predicate is a variant of [target_reg_ok] used
......@@ -631,7 +631,7 @@ Lemma return_reg_ok_incr:
Proof.
induction 1; intros; econstructor; eauto with rtlg.
Qed.
Hint Resolve return_reg_ok_incr: rtlg.
Global Hint Resolve return_reg_ok_incr: rtlg.
Lemma new_reg_return_ok:
forall s1 r s2 map sig i,
......@@ -676,7 +676,7 @@ Inductive reg_map_ok: mapping -> reg -> option ident -> Prop :=
map.(map_vars)!id = Some rd ->
reg_map_ok map rd (Some id).
Hint Resolve reg_map_ok_novar: rtlg.
Global Hint Resolve reg_map_ok_novar: rtlg.
(** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c],
between nodes [ns] and [nd], contains instructions that compute the
......
......@@ -342,7 +342,7 @@ Proof.
induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto.
Qed.
Hint Resolve areg_sound aregs_sound: va.
Global Hint Resolve areg_sound aregs_sound: va.
Lemma abuiltin_arg_sound:
forall bc ge rs sp m ae rm am,
......@@ -1912,7 +1912,7 @@ Proof.
- exact NOSTACK.
Qed.
Hint Resolve areg_sound aregs_sound: va.
Global Hint Resolve areg_sound aregs_sound: va.
(** * Interface with other optimizations *)
......
......@@ -43,12 +43,12 @@ Proof.
elim H. apply H0; auto.
Qed.
Hint Extern 2 (_ = _) => congruence : va.
Hint Extern 2 (_ <> _) => congruence : va.
Hint Extern 2 (_ < _) => extlia : va.
Hint Extern 2 (_ <= _) => extlia : va.
Hint Extern 2 (_ > _) => extlia : va.
Hint Extern 2 (_ >= _) => extlia : va.
Global Hint Extern 2 (_ = _) => congruence : va.
Global Hint Extern 2 (_ <> _) => congruence : va.
Global Hint Extern 2 (_ < _) => extlia : va.
Global Hint Extern 2 (_ <= _) => extlia : va.
Global Hint Extern 2 (_ > _) => extlia : va.
Global Hint Extern 2 (_ >= _) => extlia : va.
Section MATCH.
......@@ -4711,10 +4711,10 @@ Module VA <: SEMILATTICE.
End VA.
Hint Constructors cmatch : va.
Hint Constructors pmatch: va.
Hint Constructors vmatch: va.
Hint Resolve cnot_sound symbol_address_sound
Global Hint Constructors cmatch : va.
Global Hint Constructors pmatch: va.
Global Hint Constructors vmatch: va.
Global Hint Resolve cnot_sound symbol_address_sound
shl_sound shru_sound shr_sound
and_sound or_sound xor_sound notint_sound
ror_sound rolm_sound
......
......@@ -537,9 +537,9 @@ Inductive wt_program : program -> Prop :=
wt_fundef p.(prog_comp_env) e fd) ->
wt_program p.
Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
Hint Extern 1 (wt_int _ _ _) => exact I: ty.
Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
Global Hint Extern 1 (wt_int _ _ _) => exact I: ty.
Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
Ltac DestructCases :=
match goal with
......@@ -955,7 +955,7 @@ Proof.
destruct (classify_bool t); congruence.
Qed.
Hint Resolve check_cast_sound check_bool_sound: ty.
Global Hint Resolve check_cast_sound check_bool_sound: ty.
Lemma check_arguments_sound:
forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl.
......
......@@ -1697,7 +1697,7 @@ Qed.
End EVAL_BUILTIN_ARG.
Hint Constructors eval_builtin_arg: barg.
Global Hint Constructors eval_builtin_arg: barg.