From 6a5a17178caafdd8a4318420228c5fce47cc7a9d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 16 Sep 2024 17:10:00 +0200
Subject: [PATCH] Update the Coq files.

---
 coq/AutosubstExtra.v                  |  4 ++--
 coq/Autosubst_Env.v                   |  2 +-
 coq/Autosubst_FreeVars.v              |  4 ++--
 coq/Autosubst_IsRen.v                 |  4 ++--
 coq/CPSContextSubstitution.v          |  2 +-
 coq/CPSDefinition.v                   |  2 +-
 coq/CPSRenaming.v                     |  2 +-
 coq/DemoSyntaxReduction.v             |  4 ++--
 coq/LambdaCalculusBigStep.v           | 12 ++++++------
 coq/LambdaCalculusFreeVars.v          |  2 +-
 coq/LambdaCalculusParallelReduction.v |  4 ++--
 coq/LambdaCalculusReduction.v         | 26 +++++++++++++-------------
 coq/LambdaCalculusStandardization.v   |  4 ++--
 coq/LambdaCalculusSyntax.v            |  6 +++---
 coq/LambdaCalculusValues.v            | 10 +++++-----
 coq/MetalBigStep.v                    |  2 +-
 coq/MyTactics.v                       |  6 +++---
 coq/Option.v                          |  2 +-
 coq/README.md                         |  5 +----
 coq/STLCDefinition.v                  |  2 +-
 coq/Sequences.v                       |  2 +-
 coq/SystemFDefinition.v               |  2 +-
 coq/SystemFLemmas.v                   |  6 +++---
 23 files changed, 56 insertions(+), 59 deletions(-)

diff --git a/coq/AutosubstExtra.v b/coq/AutosubstExtra.v
index 69851e0..1650b07 100644
--- a/coq/AutosubstExtra.v
+++ b/coq/AutosubstExtra.v
@@ -194,12 +194,12 @@ End Extras.
 (* This incantation means that [eauto with autosubst] can use the tactic
    [autosubst] to prove an equality. *)
 
-Hint Extern 1 (_ = _) => autosubst : autosubst.
+Global Hint Extern 1 (_ = _) => autosubst : autosubst.
 
 (* This incantation means that [eauto with autosubst] can use the lemmas
    whose names are listed here. This is useful when an equality involves
    metavariables, so the tactic [autosubst] fails. *)
 
-Hint Resolve scons_scomp : autosubst.
+Global Hint Resolve scons_scomp : autosubst.
 
 (* -------------------------------------------------------------------------- *)
diff --git a/coq/Autosubst_Env.v b/coq/Autosubst_Env.v
index f9486c7..a9fbde5 100644
--- a/coq/Autosubst_Env.v
+++ b/coq/Autosubst_Env.v
@@ -121,7 +121,7 @@ Qed.
 
 End Env.
 
-Hint Resolve
+Global Hint Resolve
   env_ren_comp_id
   env_ren_comp_up
   env_ren_comp_prepend
diff --git a/coq/Autosubst_FreeVars.v b/coq/Autosubst_FreeVars.v
index e7b4c34..1ed1c31 100644
--- a/coq/Autosubst_FreeVars.v
+++ b/coq/Autosubst_FreeVars.v
@@ -339,8 +339,8 @@ Ltac fv :=
 
 (* A hint database to prove goals of the form [~ (closed _)] or [closed _]. *)
 
-Hint Resolve closed_ids : closed.
+Global Hint Resolve closed_ids : closed.
 
 (* -------------------------------------------------------------------------- *)
 
-Hint Resolve regular_ids regular_plus regular_upn : regular.
+Global Hint Resolve regular_ids regular_plus regular_upn : regular.
diff --git a/coq/Autosubst_IsRen.v b/coq/Autosubst_IsRen.v
index 152782b..6184d67 100644
--- a/coq/Autosubst_IsRen.v
+++ b/coq/Autosubst_IsRen.v
@@ -82,6 +82,6 @@ Qed.
 
 End Lemmas.
 
-Hint Unfold is_ren : is_ren obvious.
+Global Hint Unfold is_ren : is_ren obvious.
 
-Hint Resolve up_is_ren upn_is_ren comp_is_ren is_ren_ids : is_ren obvious.
+Global Hint Resolve up_is_ren upn_is_ren comp_is_ren is_ren_ids : is_ren obvious.
diff --git a/coq/CPSContextSubstitution.v b/coq/CPSContextSubstitution.v
index 573e1c5..c98d7d5 100644
--- a/coq/CPSContextSubstitution.v
+++ b/coq/CPSContextSubstitution.v
@@ -64,7 +64,7 @@ Proof.
   { asimpl. erewrite plus_upn by tc. autosubst. }
 Qed.
 
-Hint Resolve substc_liftc_liftc : obvious.
+Global Hint Resolve substc_liftc_liftc : obvious.
 
 (* As is the case for terms, lifting [c] by 1, then applying a substitution
    of the form [v .: ids], yields [c] again. *)
diff --git a/coq/CPSDefinition.v b/coq/CPSDefinition.v
index 3323ca6..da42779 100644
--- a/coq/CPSDefinition.v
+++ b/coq/CPSDefinition.v
@@ -368,7 +368,7 @@ Proof.
   intros. destruct v; simpl; tauto.
 Qed.
 
-Hint Resolve is_value_cpsv : is_value obvious.
+Global Hint Resolve is_value_cpsv : is_value obvious.
 
 Hint Rewrite cpsv_var cpsv_lam : cpsv.
 Ltac cpsv := autorewrite with cpsv.
diff --git a/coq/CPSRenaming.v b/coq/CPSRenaming.v
index 9af3ae3..4e690cc 100644
--- a/coq/CPSRenaming.v
+++ b/coq/CPSRenaming.v
@@ -89,4 +89,4 @@ Proof.
   eauto using upn_sigma_f, cpsv_renaming with is_ren typeclass_instances.
 Qed.
 
-Hint Resolve up_sigma_cpsv upn_sigma_cpsv : obvious.
+Global Hint Resolve up_sigma_cpsv upn_sigma_cpsv : obvious.
diff --git a/coq/DemoSyntaxReduction.v b/coq/DemoSyntaxReduction.v
index ddd0be3..4721df4 100644
--- a/coq/DemoSyntaxReduction.v
+++ b/coq/DemoSyntaxReduction.v
@@ -123,7 +123,7 @@ Inductive red : term -> term -> Prop :=
 (* The following means that [eauto with red] is allowed to apply the above
    three inference rules. *)
 
-Hint Constructors red : red.
+Local Hint Constructors red : red.
 
 (* No strategy is built into this reduction relation: it is not restricted to
    call-by-value or call-by-name. It is nondeterministic. Only weak reduction
@@ -136,7 +136,7 @@ Hint Constructors red : red.
    [autosubst] to prove an equality. It is used in the last "expert" proof
    of the lemma [red_subst] below.  *)
 
-Hint Extern 1 (_ = _) => autosubst : autosubst.
+Local Hint Extern 1 (_ = _) => autosubst : autosubst.
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/coq/LambdaCalculusBigStep.v b/coq/LambdaCalculusBigStep.v
index 910cf6d..00803be 100644
--- a/coq/LambdaCalculusBigStep.v
+++ b/coq/LambdaCalculusBigStep.v
@@ -29,7 +29,7 @@ Inductive bigcbv : term -> term -> Prop :=
     bigcbv (Let t1 t2) v
 .
 
-Hint Constructors bigcbv : bigcbv.
+Global Hint Constructors bigcbv : bigcbv.
 
 (* The tactic [invert_bigcbv] looks for a hypothesis of the form [bigcbv t v]
    and inverts it. *)
@@ -50,7 +50,7 @@ Proof.
   induction 1; eauto.
 Qed.
 
-Hint Resolve bigcbv_is_value : is_value obvious.
+Global Hint Resolve bigcbv_is_value : is_value obvious.
 
 (* -------------------------------------------------------------------------- *)
 
@@ -189,7 +189,7 @@ Inductive ebigcbv : cenv -> term -> cvalue -> Prop :=
     ebigcbv e (Let t1 t2) cv
 .
 
-Hint Constructors ebigcbv : ebigcbv.
+Global Hint Constructors ebigcbv : ebigcbv.
 
 (* -------------------------------------------------------------------------- *)
 
@@ -422,7 +422,7 @@ Proof.
   econstructor; eauto.
 Qed.
 
-Hint Resolve
+Global Hint Resolve
   use_wf_cvalue_1 use_wf_cvalue_2 prove_wf_cenv_nil prove_wf_cenv_cons
 : wf_cvalue.
 
@@ -447,7 +447,7 @@ Proof.
   { eauto 6 with wf_cvalue. }
 Qed.
 
-Hint Resolve ebigcbv_wf_cvalue : wf_cvalue.
+Global Hint Resolve ebigcbv_wf_cvalue : wf_cvalue.
 
 (* -------------------------------------------------------------------------- *)
 
@@ -565,7 +565,7 @@ Proof.
   unfold sim. eauto.
 Qed.
 
-Hint Resolve reflexive_sim transitive_sim : sim.
+Global Hint Resolve reflexive_sim transitive_sim : sim.
 
 (* This simulation relation includes the small-step relation [cbv]. *)
 
diff --git a/coq/LambdaCalculusFreeVars.v b/coq/LambdaCalculusFreeVars.v
index 38d24e5..97a6b22 100644
--- a/coq/LambdaCalculusFreeVars.v
+++ b/coq/LambdaCalculusFreeVars.v
@@ -101,7 +101,7 @@ Proof.
   unfold closed; intros; fv. tauto.
 Qed.
 
-Hint Resolve closed_Var closed_AppL closed_AppR closed_LetL : closed.
+Global Hint Resolve closed_Var closed_AppL closed_AppR closed_LetL : closed.
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/coq/LambdaCalculusParallelReduction.v b/coq/LambdaCalculusParallelReduction.v
index 1998648..20116a1 100644
--- a/coq/LambdaCalculusParallelReduction.v
+++ b/coq/LambdaCalculusParallelReduction.v
@@ -33,7 +33,7 @@ Proof.
   intros ? ? ? ? ? ? [|x]; asimpl; eauto.
 Qed.
 
-Hint Resolve pcbv_subst_up pcbv_subst_cons : red obvious.
+Global Hint Resolve pcbv_subst_up pcbv_subst_cons : red obvious.
 
 Lemma pcbv_parallel_subst:
   forall t1 t2,
@@ -61,7 +61,7 @@ Proof.
   { rewrite !subst_let. eauto 7 with obvious. }
 Qed.
 
-Hint Resolve pcbv_parallel_subst : red obvious.
+Global Hint Resolve pcbv_parallel_subst : red obvious.
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/coq/LambdaCalculusReduction.v b/coq/LambdaCalculusReduction.v
index 0830f95..8999a29 100644
--- a/coq/LambdaCalculusReduction.v
+++ b/coq/LambdaCalculusReduction.v
@@ -112,7 +112,7 @@ Inductive red (mask : mask) : term -> term -> Prop :=
     red mask (Let t1 u1) (Let t2 u2)
 .
 
-Hint Constructors red : red obvious.
+Global Hint Constructors red : red obvious.
 
 (* The following mask defines the call-by-value reduction semantics. *)
 
@@ -163,9 +163,9 @@ Notation pcbv := (red pcbv_mask).
 (* The tactic [obvious] should be able to prove goals of the form
    [red mask t1 t2], where [mask] is a known mask. *)
 
-Hint Extern 1 (cbv_mask _)  => (simpl; tauto) : red obvious.
-Hint Extern 1 (cbn_mask _)  => (simpl; tauto) : red obvious.
-Hint Extern 1 (pcbv_mask _) => (simpl; tauto) : red obvious.
+Global Hint Extern 1 (cbv_mask _)  => (simpl; tauto) : red obvious.
+Global Hint Extern 1 (cbn_mask _)  => (simpl; tauto) : red obvious.
+Global Hint Extern 1 (pcbv_mask _) => (simpl; tauto) : red obvious.
 
 Goal cbv (Let (App (Lam (Var 0)) (Var 0)) (Var 0)) (Let (Var 0) (Var 0)).
 Proof. obvious. Qed.
@@ -286,7 +286,7 @@ Proof.
   induction 2; eauto with sequences obvious.
 Qed.
 
-Hint Resolve star_cbv_AppL star_pcbv_AppL plus_pcbv_AppL star_cbv_AppR : red obvious.
+Global Hint Resolve star_cbv_AppL star_pcbv_AppL plus_pcbv_AppL star_cbv_AppR : red obvious.
 
 Lemma star_cbv_AppLR:
   forall t1 t2 u1 u2,
@@ -306,7 +306,7 @@ Proof.
   induction 1; eauto with sequences obvious.
 Qed.
 
-Hint Resolve star_cbv_AppLR star_cbv_LetL : red obvious.
+Global Hint Resolve star_cbv_AppLR star_cbv_LetL : red obvious.
 
 (* Reduction commutes with substitutions of values for variables. (This
    includes renamings.) This is true of every reduction strategy, with
@@ -363,9 +363,9 @@ Proof.
   inversion 1; is_value.
 Qed.
 
-Hint Resolve values_do_not_reduce : is_value obvious.
+Global Hint Resolve values_do_not_reduce : is_value obvious.
 
-Hint Extern 1 (False) => (eapply values_do_not_reduce) : is_value obvious.
+Global Hint Extern 1 (False) => (eapply values_do_not_reduce) : is_value obvious.
 
 Lemma is_value_irred:
   forall v,
@@ -375,7 +375,7 @@ Proof.
   intros. intro. obvious.
 Qed.
 
-Hint Resolve is_value_irred : irred obvious.
+Global Hint Resolve is_value_irred : irred obvious.
 
 (* Under every strategy, the property of being a value is preserved by
    reduction. *)
@@ -398,7 +398,7 @@ Proof.
   induction 1; is_value.
 Qed.
 
-Hint Resolve values_are_stable nonvalues_are_stable : is_value obvious.
+Global Hint Resolve values_are_stable nonvalues_are_stable : is_value obvious.
 
 (* [cbv] is deterministic. *)
 
@@ -464,7 +464,7 @@ Proof.
   intros ? ? Hirred ?. eapply Hirred. obvious.
 Qed.
 
-Hint Resolve
+Global Hint Resolve
   invert_irred_cbv_App_1
   invert_irred_cbv_App_2
   invert_irred_cbv_Let_1
@@ -496,7 +496,7 @@ Inductive stuck : term -> Prop :=
     stuck t ->
     stuck (Let t u).
 
-Hint Constructors stuck : stuck.
+Global Hint Constructors stuck : stuck.
 
 (* To go wrong is to reduce to a stuck term. *)
 
@@ -531,7 +531,7 @@ Proof.
   { congruence. }
 Qed.
 
-Hint Resolve stuck_irred : irred obvious.
+Global Hint Resolve stuck_irred : irred obvious.
 
 (* Every irreducible term either is a value or is stuck. *)
 
diff --git a/coq/LambdaCalculusStandardization.v b/coq/LambdaCalculusStandardization.v
index 4a92282..854ccf9 100644
--- a/coq/LambdaCalculusStandardization.v
+++ b/coq/LambdaCalculusStandardization.v
@@ -596,7 +596,7 @@ Inductive stdred : term -> term -> Prop :=
     stdred (Let t1 t2) (Let u1 u2)
 .
 
-Hint Constructors stdred : stdred.
+Global Hint Constructors stdred : stdred.
 
 (* A couple of more flexible constructors for [stdred]. *)
 
@@ -617,7 +617,7 @@ Proof.
   induction 1; eauto with stdred.
 Qed.
 
-Hint Resolve star_cbv_subset_stdred StdConsStar : stdred.
+Global Hint Resolve star_cbv_subset_stdred StdConsStar : stdred.
 
 (* The following lemma analyzes a reduction sequence of the form [star ipcbv
    t1 t2], where the head constructor of the term [t2] is known. In every
diff --git a/coq/LambdaCalculusSyntax.v b/coq/LambdaCalculusSyntax.v
index 49ea6bc..6e2ca37 100644
--- a/coq/LambdaCalculusSyntax.v
+++ b/coq/LambdaCalculusSyntax.v
@@ -59,7 +59,7 @@ Proof.
   rewrite <- Hid. reflexivity.
 Qed.
 
-Hint Resolve ids_implies_is_ren : is_ren obvious.
+Global Hint Resolve ids_implies_is_ren : is_ren obvious.
 
 (* The size of a term. *)
 
@@ -140,11 +140,11 @@ Ltac size_induction t :=
 (* The tactic [size] proves goals of the form [size t < n]. The tactic
    [obvious] is also extended to prove such goals. *)
 
-Hint Extern 1 (size ?t.[?sigma] < ?n) =>
+Global Hint Extern 1 (size ?t.[?sigma] < ?n) =>
   rewrite size_renaming by obvious
   : size obvious.
 
-Hint Extern 1 (size ?t < ?n) =>
+Global Hint Extern 1 (size ?t < ?n) =>
   simpl in *; lia
   : size obvious.
 
diff --git a/coq/LambdaCalculusValues.v b/coq/LambdaCalculusValues.v
index dc6f8dd..18778a4 100644
--- a/coq/LambdaCalculusValues.v
+++ b/coq/LambdaCalculusValues.v
@@ -12,7 +12,7 @@ Definition if_value {A} (t : term) (a1 a2 : A) : A :=
 Definition is_value (t : term) :=
   if_value t True False.
 
-Hint Extern 1 (is_value _) => (simpl; tauto) : is_value obvious.
+Global Hint Extern 1 (is_value _) => (simpl; tauto) : is_value obvious.
 
 (* A term either is or is not a value. *)
 
@@ -59,7 +59,7 @@ Proof.
   destruct v; simpl; eauto.
 Qed.
 
-Hint Resolve is_value_renaming is_nonvalue_renaming : is_value obvious.
+Global Hint Resolve is_value_renaming is_nonvalue_renaming : is_value obvious.
 
 Ltac is_value :=
   eauto with is_value.
@@ -141,7 +141,7 @@ Proof.
   intros. intro x. asimpl. is_value.
 Qed.
 
-Hint Resolve is_value_subst_up is_value_subst_upn is_value_subst_renaming
+Global Hint Resolve is_value_subst_up is_value_subst_upn is_value_subst_renaming
   : is_value obvious.
 
 Lemma values_are_preserved_by_value_substitutions:
@@ -161,7 +161,7 @@ Proof.
   destruct t; simpl; tauto.
 Qed.
 
-Hint Resolve
+Global Hint Resolve
   is_value_subst_ids
   is_value_subst_cons
   values_are_preserved_by_value_substitutions
@@ -176,4 +176,4 @@ Proof.
   intros ? [ xi ? ]. subst. eauto with is_value.
 Qed.
 
-Hint Resolve is_ren_is_value_subst : is_value obvious.
+Global Hint Resolve is_ren_is_value_subst : is_value obvious.
diff --git a/coq/MetalBigStep.v b/coq/MetalBigStep.v
index 59bf36f..b390c13 100644
--- a/coq/MetalBigStep.v
+++ b/coq/MetalBigStep.v
@@ -74,7 +74,7 @@ Inductive mbigcbv : menv -> metal -> mvalue -> Prop :=
     mbigcbv e (MPi i t) mv
 .
 
-Hint Constructors mbigcbv : mbigcbv.
+Global Hint Constructors mbigcbv : mbigcbv.
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/coq/MyTactics.v b/coq/MyTactics.v
index d47559a..f7284c6 100644
--- a/coq/MyTactics.v
+++ b/coq/MyTactics.v
@@ -149,9 +149,9 @@ Ltac injections :=
 (* The following incantations are suppose to allow [eauto with lia] to solve
    goals of the form [_ < _] or [_ <= _]. *)
 
-Hint Extern 1 (_ <  _) => lia : lia.
-Hint Extern 1 (_ <= _) => lia : lia.
-Hint Resolve lt_n_S : lia.
+Global Hint Extern 1 (_ <  _) => lia : lia.
+Global Hint Extern 1 (_ <= _) => lia : lia.
+Global Hint Resolve lt_n_S : lia.
 
 (* -------------------------------------------------------------------------- *)
 
diff --git a/coq/Option.v b/coq/Option.v
index 5ed2a2e..194ac0a 100644
--- a/coq/Option.v
+++ b/coq/Option.v
@@ -115,6 +115,6 @@ Proof.
   { eauto using prove_less_defined_None. }
 Qed.
 
-Hint Resolve
+Global Hint Resolve
   prove_less_defined_None reflexive_less_defined prove_less_defined_bind
 : less_defined.
diff --git a/coq/README.md b/coq/README.md
index e24a499..33d2eac 100644
--- a/coq/README.md
+++ b/coq/README.md
@@ -4,8 +4,5 @@ please use [this installation script](coq/installation.sh).
 You can then check the proofs as follows:
 ```
   make _CoqProject
-  make -j4
+  make -j
 ```
-
-The author of these proofs is [François Pottier](francois.pottier@inria.fr).
-The files in this directory are covered by the [MIT License](LICENSE).
diff --git a/coq/STLCDefinition.v b/coq/STLCDefinition.v
index f226cf6..f78e1df 100644
--- a/coq/STLCDefinition.v
+++ b/coq/STLCDefinition.v
@@ -75,4 +75,4 @@ The following hint allows `eauto with jt` to apply the above typing rules.
 
 |*)
 
-Hint Constructors jt : jt.
+Global Hint Constructors jt : jt.
diff --git a/coq/Sequences.v b/coq/Sequences.v
index 13c8552..609f0a4 100644
--- a/coq/Sequences.v
+++ b/coq/Sequences.v
@@ -316,5 +316,5 @@ End DETERMINISM.
 
 End SEQUENCES.
 
-Hint Resolve star_refl star_step star_one star_trans plus_left plus_one
+Global Hint Resolve star_refl star_step star_one star_trans plus_left plus_one
              plus_star plus_star_trans star_plus_trans plus_right: sequences.
diff --git a/coq/SystemFDefinition.v b/coq/SystemFDefinition.v
index 508b5bf..252674d 100644
--- a/coq/SystemFDefinition.v
+++ b/coq/SystemFDefinition.v
@@ -87,4 +87,4 @@ The following hint allows `eauto with jf` to apply the above typing rules.
 
 |*)
 
-Hint Constructors jf : jf.
+Global Hint Constructors jf : jf.
diff --git a/coq/SystemFLemmas.v b/coq/SystemFLemmas.v
index 10f456f..4a88f08 100644
--- a/coq/SystemFLemmas.v
+++ b/coq/SystemFLemmas.v
@@ -58,7 +58,7 @@ The following hint allows `eauto with jtn` to apply the above typing rules.
 
 |*)
 
-Hint Constructors jtn : jtn.
+Global Hint Constructors jtn : jtn.
 
 (*|
 -----------------------------------------
@@ -84,7 +84,7 @@ The following hint allows `eauto with jt` to exploit the fact that
 
 |*)
 
-Hint Unfold jt : jt.
+Global Hint Unfold jt : jt.
 
 (*|
 
@@ -142,7 +142,7 @@ The following hint allows `eauto with jt` to use the above lemmas.
 
 |*)
 
-Hint Resolve JTVar JTLam JTApp JTTyAbs JTTyApp : jt.
+Global Hint Resolve JTVar JTLam JTApp JTTyAbs JTTyApp : jt.
 
 (*|
 
-- 
GitLab