Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.

5 files changed, 6 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index b80e0bb0e4..e28314cada 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope.
 Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D')
   := admit.
 
-Global Class FunctorApplicationInterpretable
+Class FunctorApplicationInterpretable
        {C D} (F : Functor C D)
        {argsT : Type} (args : argsT)
        {T : Type} (rtn : T)
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
index 19551dc92e..72bc04e05e 100644
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F'
   := Build_NaturalTransformation (F o G) (F' o G)
                                  (fun c => T (G c))
                                  admit.
-Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
+Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
 
 Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
 Notation "T 'o' U"
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
index a80d075f69..cd6539b51c 100644
--- a/test-suite/bugs/closed/HoTT_coq_120.v
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -89,7 +89,7 @@ Definition set_cat : PreCategory
   := @Build_PreCategory hSet
                         (fun x y => forall _ : x, y)%core
                         (fun _ _ _ f g x => f (g x))%core.
-Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
+Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
 Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
 Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v
index 317efb0b32..f00d2fcf09 100644
--- a/test-suite/bugs/closed/bug_3427.v
+++ b/test-suite/bugs/closed/bug_3427.v
@@ -146,7 +146,7 @@ Section Univalence.
     := (equiv_path A B)^-1 f.
 End Univalence.
 
-Local Inductive minus1Trunc (A :Type) : Type :=
+Inductive minus1Trunc (A :Type) : Type :=
   min1 : A -> minus1Trunc A.
 
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0.
diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v
index 5db0f81cc5..5f9d42f5f7 100644
--- a/test-suite/bugs/closed/bug_7795.v
+++ b/test-suite/bugs/closed/bug_7795.v
@@ -52,6 +52,8 @@ Definition hh:
          false = true.
 Admitted.
 
+Require Import Program.
+
 Set Program Mode. (* removing this line prevents the bug *)
 Obligation Tactic := repeat t_base.