Merge pull request #6 from coq-community/fix-8.10-deprecations

fix a bunch of deprecations on Coq 8.10

ch13_co_inductive_types/SRC/Tree_Inf.v

@@ -42,7 +42,7 @@ Inductive Finite (A:Type) :(LTree A)->Prop :=
                                       Finite (LBin a t1 t2).
 
 Hint Resolve Finite_leaf Finite_bin SomeFin_leaf 
-SomeFin_left  SomeFin_right.
+SomeFin_left  SomeFin_right : core.
 
 
 

ch13_co_inductive_types/SRC/chap13.v

@@ -7,7 +7,7 @@ CoInductive LList (A:Type) : Type :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 (** Tests :
 Check (LCons 1 (LCons 2 (LCons 3 LNil))).
@@ -902,7 +902,7 @@ Definition trans (q:st) (x:acts) : list st :=
 (* a toy automaton *)
 Definition A1 := mk_auto q0 trans.
 
-Hint Unfold A1.
+Hint Unfold A1 : core.
 
 Lemma no_deadlocks : forall q:states A1, ~ deadlock  A1 q.
 Proof.

ch13_co_inductive_types/SRC/infinite_impred.v

@@ -5,7 +5,7 @@ CoInductive LList (A:Type) : Type :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 CoInductive Infinite {A:Type} : LList A -> Prop :=
     Infinite_LCons :

ch13_co_inductive_types/SRC/infinite_impred_prelude.v

@@ -5,13 +5,13 @@ CoInductive LList (A:Type) : Type :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 CoInductive Infinite {A:Type} : LList A -> Prop :=
     Infinite_LCons :
       forall (a:A) (l:LList A), Infinite l -> Infinite (LCons a l).
 
-Hint Constructors Infinite.
+Hint Constructors Infinite : core.
 
 
 

ch13_co_inductive_types/SRC/list_inject.v

@@ -6,7 +6,7 @@ CoInductive LList (A:Type) : Type :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Fixpoint llist_injection {A:Type} (l:list A) :  LList A :=
   match l with

ch14_fundations_of_inductive_types/SRC/chap14.v

@@ -346,7 +346,7 @@ Fixpoint n_sum_values (t:ntree Z) : Z :=
   | ncons _ t tl => n_sum_values t + n_sum_values_l tl
   end.
 
-Hint Resolve occurs_branches occurs_root Zplus_le_compat.
+Hint Resolve occurs_branches occurs_root Zplus_le_compat : core.
 
 Theorem greater_values_sum :
  forall t:ntree Z,

ch15_general_recursion/SRC/chap15.v

@@ -159,7 +159,7 @@ Proof.
   intros x v H; generalize (double_div2_le x);  omega.
 Qed.
 
-Hint Resolve div2_le f_lemma double_div2_le.
+Hint Resolve div2_le f_lemma double_div2_le : core.
 
 Definition nested_F :
   forall x:nat, (forall y:nat, y < x -> {v:nat | v <= y}) -> {v:nat | v <= x }.

ch15_general_recursion/SRC/not_decreasing.v

@@ -16,7 +16,7 @@ Section Sequences.
  Qed.
 
  Hypothesis W : well_founded R.
- Hint Resolve W.
+ Hint Resolve W : core.
 
  Section seq_intro.
   Variable seq : nat -> A. 

ch5_everydays_logic/SRC/leibniz.v

@@ -24,7 +24,7 @@ Section leibniz.
  Qed.
 
 
- Hint Resolve leibniz_trans leibniz_sym leibniz_refl. 
+ Hint Resolve leibniz_trans leibniz_sym leibniz_refl : core.
 
  Theorem leibniz_equiv : equiv A leibniz.
  Proof.

ch6_inductive_data/SRC/exo_frac.v

@@ -69,7 +69,7 @@ Proof.
    now  rewrite (Zmult_comm v (Z_of_nat b)).
 Qed.
 
-Hint Resolve b_one b_d b_n.
+Hint Resolve b_one b_d b_n : core.
 
 Inductive simplified : nat*nat -> Prop :=
   mk_simpl : forall a b : nat, bezout a b -> simplified (a, b).

ch7_tactics_automation/SRC/chap7.v

@@ -264,7 +264,7 @@ Section primes.
   end.
 Open Scope nat_scope.
 
-Hint Resolve lt_O_Sn.
+Hint Resolve lt_O_Sn : core.
 
 Ltac check_lt_not_divides :=
   match goal with

ch8_inductive_predicates/SRC/chap8.v

@@ -337,7 +337,7 @@ Open Scope nat_scope.
 Inductive is_0_1 : nat->Prop :=
   is_0 : is_0_1 0 | is_1 : is_0_1 1.
 
-Hint Resolve is_0 is_1 .
+Hint Resolve is_0 is_1 : core.
 
 Lemma sqr_01 : forall x:nat, is_0_1 x -> is_0_1 (x * x).
 Proof.

ch8_inductive_predicates/SRC/even.v

@@ -5,7 +5,7 @@ Inductive even : nat -> Prop :=
   | plus_2_even : forall n:nat, even n -> even (S (S n)).
 
 
-Hint Constructors even.
+Hint Constructors even : core.
 
 Fixpoint mult2 (n:nat) : nat :=
   match n with
@@ -23,7 +23,7 @@ Proof.
  intros n p Heven_n; induction  Heven_n; simpl; auto.
 Qed.
 
-Hint Resolve sum_even.
+Hint Resolve sum_even : core.
 
 Lemma square_even : forall n:nat, even n -> even (n * n).
 Proof.

ch8_inductive_predicates/SRC/impredicative.v

@@ -35,7 +35,7 @@ Inductive sorted : list A -> Prop :=
 | sorted2 : forall (x1 x2:A)(l':list A),
               R x1 x2 -> sorted  (x2::l') -> sorted  (x1::x2::l').
 
-Hint Constructors sorted.
+Hint Constructors sorted : core.
 
 Definition impredicative_sorted (l:list A) : Prop :=
   forall P :  list A -> Prop,
@@ -69,7 +69,7 @@ Proof.
  apply Hs; auto.
 Qed.
 
-Hint Resolve isorted0 isorted1 isorted2.
+Hint Resolve isorted0 isorted1 isorted2 : core.
 
 
 (* Proof of the equivalence between both definitions *)
@@ -114,7 +114,7 @@ Proof.
   intros n m Hle P Hn Hs; apply Hs; apply Hle; auto.
 Qed.
 
-Hint Resolve impredicative_le_n impredicative_le_S.
+Hint Resolve impredicative_le_n impredicative_le_S : core.
 
 Theorem le_to_impredicative :
  forall n p, n <= p -> impredicative_le n p.
@@ -152,7 +152,7 @@ Proof.
  unfold impredicative_or; auto.
 Qed.
 
-Hint Resolve impredicative_or_intro1 impredicative_or_intro2.
+Hint Resolve impredicative_or_intro1 impredicative_or_intro2 : core.
 
 Theorem or_to_impredicative : forall A B, A \/ B -> impredicative_or A B.
 Proof.

ch8_inductive_predicates/SRC/last.v

@@ -9,7 +9,7 @@ Inductive last (a:A) : list A -> Prop :=
    | last_tl : forall (b:A) (l:list A), last a l -> last a (b :: l).
 
 
-Hint Constructors last.
+Hint Constructors last : core.
 
 Fixpoint last_fun (l:list A) : option A :=
   match l with

ch8_inductive_predicates/SRC/le_prime.v

@@ -4,7 +4,7 @@ Inductive le' : nat -> nat -> Prop :=
   | le'_0_p : forall p:nat, le' 0 p
   | le'_Sn_Sp : forall n p:nat, le' n p -> le' (S n) (S p).
 
-Hint Constructors le'.
+Hint Constructors le' : core.
 
 Lemma le'_n : forall n : nat, le' n n.
 Proof.
@@ -18,7 +18,7 @@ Proof.
   -  intros p Hp; inversion_clear Hp;  auto.
 Qed.
 
-Hint Resolve le'_n le'_n_Sp.
+Hint Resolve le'_n le'_n_Sp : core.
 
 Lemma le_le' : forall n p: nat, le n p -> le' n p.
 Proof.

ch8_inductive_predicates/SRC/non_inductive_sorted.v

@@ -16,7 +16,7 @@ Definition sorted' (l:list A) :=
     l = l1 ++ (n1 :: n2 ::l2) -> 
     R n1 n2.
 
-Hint Constructors sorted.
+Hint Constructors sorted : core.
 
 
 (** Let us prove that sorted' satisfies the constructors of sorted 
@@ -46,7 +46,7 @@ Proof.
     intros Heq' Heqx; apply (Hs l1' l2); trivial.
 Qed.
 
-Hint Resolve sorted'0 sorted'1 sorted'2.
+Hint Resolve sorted'0 sorted'1 sorted'2 : core.
 
 Lemma sorted'_inv : forall a l, sorted' (a::l) -> sorted' l.
 Proof.
@@ -69,4 +69,4 @@ Proof.
    *  apply IHl'; apply (sorted'_inv _ _ H).
 Qed.
 
-End Definitions.
+End Definitions.

ch8_inductive_predicates/SRC/palindrome.v

@@ -17,7 +17,7 @@ Section mirror.
        forall (a:A) (l m:list A),
          palindrome l -> remove_last a m l -> palindrome (a :: m).
 
- Hint Constructors remove_last palindrome.  
+ Hint Constructors remove_last palindrome : core.
 
 
  Lemma ababa : forall a b:A, palindrome (a :: b :: a :: b :: a :: nil).

ch8_inductive_predicates/SRC/parsing.v

@@ -77,7 +77,7 @@ Proof.
  -  simpl ; intros t1 H1 t2 H2; apply wp_o_head_c; trivial.
 Qed.
 
-Hint Resolve wp_nil wp_concat wp_encapsulate wp_o_head_c wp_o_tail_c wp_oc.
+Hint Resolve wp_nil wp_concat wp_encapsulate wp_o_head_c wp_o_tail_c wp_oc : core.
 
 Fixpoint bin_to_string' (t:bin) : list par :=
   match t with
@@ -154,7 +154,7 @@ Proof.
     simpl; apply wp'_cons; auto.
 Qed.
 
-Hint Resolve wp'_nil wp'_cons wp'_concat.
+Hint Resolve wp'_nil wp'_cons wp'_concat : core.
 
 (* This is the other constructor of wp, also satisfied by wp'. *)
 
@@ -195,7 +195,7 @@ Inductive wp'' : list par -> Prop :=
       forall l1 l2:list par,
         wp'' l1 -> wp'' l2 -> wp'' (l1 ++ open :: l2 ++ close :: nil).
 
-Hint Resolve wp''_nil wp''_cons.
+Hint Resolve wp''_nil wp''_cons : core.
 
 (* Obviously this one also satisfies the concatenation property. *)
 
@@ -216,7 +216,7 @@ Proof.
  intros l H; change (wp'' (nil ++ open :: l ++ close :: nil));
  auto.
 Qed.
-Hint Resolve wp''_concat wp''_encapsulate.
+Hint Resolve wp''_concat wp''_encapsulate : core.
 
 (* solution to exercise \ref{exo-wp-4} *)
 

ch9_function_specification/SRC/chap9.v

@@ -172,7 +172,7 @@ Section minimal_specification_strengthening.
   Proof.
   intro n; exists 1; simpl; auto.
  Qed.
- Hint Resolve divides_refl.
+ Hint Resolve divides_refl : core.
 
  Check (fun E:nat=>  fun n:nat => if prime_test n then n else E).
 
@@ -406,7 +406,7 @@ Proof.
 Qed.
 Hint Resolve rem_odd_ge_interval rem_even_ge_interval
  rem_odd_lt_interval rem_even_lt_interval rem_1_odd_interval
- rem_1_even_interval rem_1_1_interval.
+ rem_1_even_interval rem_1_1_interval : core.
 
 Ltac div_bin_tac arg1 arg2 :=
   elim arg1;

tutorial_inductive_co_inductive_types/SRC/RecTutorial.v

@@ -1053,7 +1053,7 @@ infiniteproof map_iterate'.
  reflexivity.
 Qed.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).