Fix deprecations from rocq master

Author: mattam82

examples/AlmostFull.v

@@ -684,16 +684,16 @@ Section SCT.
       intros n k'' g b f. intros H.
       intros gz [x rx] y.
       specialize (H (x, rx) y rx y). simpl.
-      rewrite H. clear H.
+      rw H. clear H.
       split.
       + intros [xlt relr].
-        intros f'. depelim f'. rewrite gz. apply xlt. apply relr.
+        intros f'. depelim f'. rw gz. apply xlt. apply relr.
       + intros Hf. split.
-        specialize (Hf fz). rewrite gz in Hf. apply Hf.
+        specialize (Hf fz). rw gz in Hf. apply Hf.
         intros f'. apply Hf.
       + intros n k'' g gf x y.
         split. intros [].
-        intros f. specialize (f fz). now rewrite gf in f.
+        intros f. specialize (f fz). now rw gf in f.
     Qed.
 
   Lemma graph_relation_spec {k : nat} (G : graph k) :
@@ -706,7 +706,7 @@ Section SCT.
                     | None => False
                     end).
     Proof.
-      unfold graph_relation. intros x y. now rewrite k_related_spec.
+      unfold graph_relation. intros x y. now rw k_related_spec.
     Qed.
 
   Definition approximates {k} (G : graph k) (R : relation (k_tuple_type k)) :=
@@ -732,13 +732,13 @@ Section SCT.
     approximates (G0 ⋅ G1) (compose_rel R0 R1).
   Proof.
     unfold approximates. intros ag0 ag1.
-    intros x z [y [Hxy Hyz]]. rewrite graph_relation_spec.
+    intros x z [y [Hxy Hyz]]. rw graph_relation_spec.
     intros f. specialize (ag0 _ _ Hxy). specialize (ag1 _ _ Hyz).
     rewrite -> graph_relation_spec in ag0, ag1. specialize (ag0 f).
-    funelim (graph_compose G0 G1 f). now rewrite Heq in ag0.
-    rewrite Heq0 in ag0. specialize (ag1 arg1). rewrite Heq in ag1.
+    funelim (graph_compose G0 G1 f). now rw Heq in ag0.
+    rw Heq0 in ag0. specialize (ag1 arg1). rw Heq in ag1.
     destruct weight, weight'; simpl;  try lia.
-    specialize (ag1 arg1). now rewrite Heq in ag1.
+    specialize (ag1 arg1). now rw Heq in ag1.
   Qed.
 
   Equations fin_union {A n} (f : fin n -> relation A) : relation A :=
@@ -752,10 +752,10 @@ Section SCT.
     intros [k _]. depelim k.
     split. intros [Hfz|Hfs].
     now exists fz.
-    specialize (H x y x y). rewrite -> H in Hfs.
+    specialize (H x y x y). rw H in Hfs.
     destruct Hfs. now exists (fs x0).
     intros [k Hk]. depelim k. now left. right.
-    rewrite (H x y). now exists k.
+    rw (H x y). now exists k.
   Qed.
 
   Equations fin_all k (p : fin k -> bool) : bool :=
@@ -770,7 +770,7 @@ Section SCT.
     destruct (p fz) eqn:pfz. simpl. specialize (IHk (fun f => p (fs f))).
     simpl in IHk. destruct IHk; constructor. intros f; depelim f; auto.
     intro Hf. apply n. intros f'. apply Hf.
-    simpl. constructor. intros H. specialize (H fz). rewrite pfz in H. discriminate.
+    simpl. constructor. intros H. specialize (H fz). rw pfz in H. discriminate.
   Qed.
 
   Definition graph_eq {k} (g g' : graph k) : bool :=
@@ -813,7 +813,7 @@ Section SCT.
     forall x y, list_union (rs ++ rs') x y <-> list_union rs x y \/ list_union rs' x y.
   Proof.
     induction rs; intros; simpl; simp list_union; intuition.
-    rewrite -> IHrs in H0. intuition.
+    rw IHrs in H0. intuition.
   Qed.
 
   Equations map_k_tuple k (p : k_tuple_type k) (f : fin k -> nat) : k_tuple_type k :=
@@ -878,7 +878,7 @@ Section SCT.
       intuition.
       + revert H. clear -inS inScomp Ingi.
         induction famgi. simpl. intros [].
-        simpl. rewrite in_app_iff in_map_iff.
+        simpl. rw in_app_iff in_map_iff.
         intros [[x [<- Inx]]| Ing]. apply inScomp. intuition auto.
         apply Ingi. constructor. auto.
         apply IHfamgi; auto. intros.
@@ -958,9 +958,9 @@ Section SCT.
   Proof.
     induction k. unfold TI_graph. do 2 red in G. intros f; depelim f.
     intros f. depelim f. simp TI_graph graph_compose.
-    destruct (G fz) as [[weight d]|]; simpl; try easy. now rewrite orb_false_r.
+    destruct (G fz) as [[weight d]|]; simpl; try easy. now rw orb_false_r.
     simp TI_graph graph_compose.
-    destruct (G (fs f)) as [[weight d]|]; simpl; trivial. now rewrite orb_false_r.
+    destruct (G (fs f)) as [[weight d]|]; simpl; trivial. now rw orb_false_r.
   Qed.
 
   Definition TI k : relation (k_tuple_type k) := graph_relation (TI_graph k).
@@ -977,10 +977,10 @@ Section SCT.
         intros Hg. pose proof Hg. rewrite -> graph_relation_spec in H.
         intros. pose (H fz). simpl in y0. intuition.
         assert (graph_relation (TI_graph k) rx ry).
-        rewrite graph_relation_spec. intros. clear y0. specialize (H (fs f)). simpl in H.
+        rw graph_relation_spec. intros. clear y0. specialize (H (fs f)). simpl in H.
         unfold TI_graph. destruct k. depelim f. auto.
         do 2 red in IHk. simpl in IHk. rewrite <- IHk. apply H0.
-      + intros [Hle Hi]. unfold TI. rewrite graph_relation_spec.
+      + intros [Hle Hi]. unfold TI. rw graph_relation_spec.
         intros. depelim f. simpl. auto. simpl.
         do 2 red in IHk. simpl in IHk. rewrite <- IHk in Hi.
         red in Hi. rewrite -> graph_relation_spec in Hi.
@@ -990,7 +990,7 @@ Section SCT.
 
   #[global] Instance TI_AlmostFull k : AlmostFull (TI k).
   Proof.
-    rewrite TI_intersection_equiv.
+    rw TI_intersection_equiv.
     induction k. simpl. red. red. exists ZT. simpl. intros. exact I.
     simpl. apply af_interesection.
     apply (AlmostFull_MR Nat.le). apply almost_full_le.
@@ -1012,11 +1012,11 @@ Section SCT.
       exists x. intuition. }
     pose (compose_approximates G (TI_graph k) T (TI k)).
     forward a; auto. forward a; auto. unfold TI. red. intuition.
-    rewrite TI_compose' in a.
+    rw TI_compose' in a.
     apply (approximates_power n) in a.
     specialize (a x x). specialize (a H0).
     rewrite -> graph_relation_spec in a. specialize (a f).
-    rewrite eqpow in a. lia.
+    rw eqpow in a. lia.
   Qed.
 
   Theorem size_change_termination {k} (n : nat)
@@ -1146,7 +1146,7 @@ Section SCT.
   Lemma existsb_spec {A} (p : A -> bool) l : reflect (exists x, In x l /\ p x = true) (existsb p l).
   Proof.
     destruct existsb eqn:Heq. constructor. now apply existsb_exists in Heq.
-    constructor. intro. apply existsb_exists in H. rewrite Heq in H; discriminate.
+    constructor. intro. apply existsb_exists in H. rw Heq in H; discriminate.
   Qed.
   Lemma eqb_refl {A} `{E:Eq A} (a : A) : eqb a a = true.
   Proof. destruct (eqb_spec a a); intuition. Qed.
@@ -1227,7 +1227,7 @@ Section SCT.
     + intros * H l Haux.
 (*      forward H. red. intuition.
       specialize (H l Haux). apply H. auto with datatypes.
-      rewrite app_nil_r. red. intuition. intuition.
+      rw app_nil_r. red. intuition. intuition.
     + intros * n * tracc l' [= <-]. simpl. split. intuition.
       intros inclgs incltrgs becacc.
       intuition. red. intuition. red.
@@ -1373,6 +1373,7 @@ Equations T_graphs (f : fin 2) : graph 2 :=
   T_graphs (fs fz) := T_graph_r.
 
 Definition gnlex : (nat * nat) -> nat.
+Proof.
   assert (sct:=size_change_termination 2 T_rel T_graphs). forward sct.
   intros f; depelim f. apply approximates_T_l. depelim f. apply approximates_T_r. depelim f.
   specialize (sct T_trans_clos). forward sct. apply (compute_transitive_closure_spec 10). reflexivity.
@@ -1402,17 +1403,18 @@ Print Assumptions gnlex. *)
 (* Eval native_compute in gnlex (4, 3). *)
 
 Lemma gnlex_0_l y : gnlex (0, y) = 1.
-Admitted.
+Proof. Admitted.
 
 Lemma gnlex_0_r x : gnlex (x, 0) = 1.
-Admitted.
+Proof.  Admitted.
 
 
 Lemma gnlex_S x y : gnlex (S x, S y) = gnlex (S y, y) + gnlex (S y, x).
-Admitted.
+Proof. Admitted.
 
 Lemma gnlex_S_test x y : exists foo, gnlex (S x, S y) = foo.
-  eexists. rewrite gnlex_S. destruct y. rewrite gnlex_0_r.
-  destruct x. rewrite gnlex_0_r. reflexivity.
-  rewrite gnlex_S. rewrite gnlex_0_r. destruct x. admit. rewrite gnlex_S.
+Proof. 
+  eexists. rw gnlex_S. destruct y. rw gnlex_0_r.
+  destruct x. rw gnlex_0_r. reflexivity.
+  rw gnlex_S. rw gnlex_0_r. destruct x. admit. rw gnlex_S.
 Admitted.

examples/HoTT_light.v

@@ -196,22 +196,21 @@ Notation "p ..1" := (pr1_path p) (at level 1).
 
 Definition pr2_path {A} `{P : A -> Type} {u v : sigma P} (p : u = v)
 : p..1 # u.2 = v.2.
-  destruct p. apply 1.
-Defined.
+Proof. destruct p. apply 1. Defined.
 
 Notation "p ..2" := (pr2_path p) (at level 1).
 
 Definition eta_path_sigma_uncurried {A} `{P : A -> Type} {u v : sigma P}
            (p : u = v) : path_sigma_uncurried _ _ (p..1, p..2) = p.
-  destruct p. apply 1.
-Defined.
+Proof. destruct p. apply 1. Defined.
 
 Definition eta_path_sigma A `{P : A -> Type} {u v : sigma P} (p : u = v)
 : path_sigma _ _ (p..1) (p..2) = p
   := eta_path_sigma_uncurried p.
 
 Definition path_sigma_equiv {A : Type} (P : A -> Type) (u v : sigma P):
   IsEquiv (path_sigma_uncurried u v).
+Proof.
   unshelve refine (BuildIsEquiv _ _ _).
   - exact (fun r => (r..1, r..2)).
   - intro. apply eta_path_sigma_uncurried.
@@ -409,6 +408,7 @@ Defined.
 
 Definition transport_inv A {P : A -> Type} (x y :A) (e : x = y) (u:P x) v:
   u = e^ # v -> e # u = v.
+Proof.
   destruct e. exact id. 
 Defined.
 
@@ -458,6 +458,7 @@ Definition path_contr {A} {H:Contr A} (x y : A) : x = y
   := concat (id_sym (@contr _ H x)) (@contr _ H y).
 
 Definition path2_contr {A} {H:Contr A} {x y : A} (p q : x = y) : p = q.
+Proof.
   assert (K : forall (r : x = y), r = path_contr x y).
   intro r; destruct r; symmetry; now apply concat_Vp.
   apply (transitivity (y:=path_contr x y)).

examples/ordinals.v

@@ -3,25 +3,28 @@ From Stdlib Require Import Eqdep_dec.
 From Stdlib Require Import Peano_dec.
 From Stdlib Require Import List.
 From Stdlib Require Import Recdef.
-
+Set Warnings "-missing-proof-command".
 (**
   Arithmétique
 *)
 
 (* Sur la soustraction (entière) *)
 Lemma minus_Sn_n : forall (n:nat), (minus (S n) n) = (S 0).
+Proof.
 induction n; auto.
 Qed.
 
 Lemma lt_S_r : forall (n1 n2:nat),
   (lt n1 n2) -> exists (n:nat), n2 = (S n).
+Proof.
 destruct n2.
   intro. exfalso. apply (Nat.nlt_0_r n1). assumption.
   intro. exists n2. trivial.
 Qed.
 
 Lemma minus_lt_S : forall (n1 n2:nat),
   (lt n1 n2) -> exists (n:nat), (minus n2 n1) = (S n).
+Proof.
 intros. elim (lt_S_r n1 n2 H). intros n H1. rewrite H1.
 exists (minus n n1). rewrite Nat.sub_succ_l.
   trivial.
@@ -30,12 +33,14 @@ Qed.
 
 (* Sur l'ordre strict 'lt' *)
 Lemma lt_1_0 : forall (n:nat), (lt n 1) -> (n=0).
+Proof.
 destruct n.
   auto.
   intro. inversion H. exfalso. apply (Nat.nle_succ_0 (S n)). assumption.
 Qed.
 
 Lemma lt_S_case : forall (m n:nat), (lt m (S n)) -> (lt m n) \/ (m=n).
+Proof.
 intros m n. generalize m. induction n.
   intros. rewrite (lt_1_0 m0 H). tauto.
   destruct m0.    
@@ -44,13 +49,15 @@ intros m n. generalize m. induction n.
 Qed.
 
 Lemma not_lt_Sn_n : forall (n:nat), not (lt (S n) n).
+Proof.
 induction n.
   auto with arith.
   intro. auto with arith.
 Qed.
 
 (* Sur l'ordre large 'le' *)
 Lemma not_le_Sn_n : forall (n:nat), not (le (S n) n).
+Proof.
 induction n.
   auto with arith.
   intro. auto with arith.
@@ -59,6 +66,7 @@ Qed.
 (* Cas sur les entiers *)
 Lemma nat_compare_case : forall (n1 n2:nat),
  (lt n1 n2) \/ (n1=n2) \/ (lt n2 n1).
+Proof.
 induction n1.
   destruct n2.
     tauto.
@@ -878,6 +886,7 @@ Qed.
 
 Lemma rlex_nat3_4 : forall (x y z m : nat),
   (rlex_nat3 (S x, y, m) (S x, S y, z)).
+Proof.
 unfold rlex_nat3. unfold make_mwlt. destruct y.
   intros. simpl. apply wlt_wlt. 
     auto with arith.

examples/polynomials.v

@@ -850,16 +850,20 @@ Ltac bool_tauto_with f :=
 (** Examples *)
 
 Goal forall a b, andb a b = andb b a.
+Proof.
   bool_tauto_with @correctness_heyting.
 Qed.
 Goal forall a b, andb (negb a) (negb b) = negb (orb a b).
+Proof.
   bool_tauto_with @correctness_heyting.
 Qed.
 Goal forall a b, orb (negb a) (negb b) = negb (andb a b).
+Proof.
   bool_tauto_with @correctness_heyting.
 Qed.
 
 Example neg_involutive: forall a, orb (negb a) a = true.
+Proof.
 Fail bool_tauto_with @correctness_heyting.
 bool_tauto_with @correctness_classical.
 Qed.

src/ederive.ml

@@ -42,17 +42,17 @@ module StringSet = Set.Make(StringOrd)
 (** We keep a table of which derives have been performed yet for a given global reference. *)
 type derive_instance = (string * Names.GlobRef.t)
 
-type derive_instance_map = StringSet.t Names.GlobRef.Map.t
+type derive_instance_map = StringSet.t Names.GlobRef.Map_env.t
 
-let derived_instances : derive_instance_map ref = Summary.ref Names.GlobRef.Map.empty ~name:"derived-instances"
+let derived_instances : derive_instance_map ref = Summary.ref Names.GlobRef.Map_env.empty ~name:"derived-instances"
 
 let cache_instance (derive, gr) =
   let grderives = 
-    match Names.GlobRef.Map.find_opt gr !derived_instances with
+    match Names.GlobRef.Map_env.find_opt gr !derived_instances with
     | Some s -> s
     | None -> StringSet.empty
   in
-  derived_instances := Names.GlobRef.Map.add gr (StringSet.add derive grderives) !derived_instances
+  derived_instances := Names.GlobRef.Map_env.add gr (StringSet.add derive grderives) !derived_instances
 
 let subst_instance (subst, (derive, gr)) =
   (derive, fst (Globnames.subst_global subst gr))
@@ -75,7 +75,7 @@ let register_instance decl =
 
 let check_derive s gr =
   try
-    let grds = Names.GlobRef.Map.find gr !derived_instances in
+    let grds = Names.GlobRef.Map_env.find gr !derived_instances in
     StringSet.mem s grds
   with Not_found -> false
 

src/equations.ml

@@ -40,7 +40,7 @@ let define_unfolding_eq ~pm env evd (flags : flags)  p unfp prog prog' ei hook =
                  user_obls = Id.Set.union prog.program_split_info.user_obls info'.user_obls } in
   let () = inline_helpers info in
   let funf_cst = match info'.term_id with GlobRef.ConstRef c -> c | _ -> assert false in
-  let () = if PolyFlags.univ_poly flags.poly then evd := Evd.from_ctx info'.term_ustate in
+  let () = if PolyFlags.univ_poly flags.poly then evd := Evd.from_ustate info'.term_ustate in
   let funfc = e_new_global evd info'.term_id in
   let unfold_eq_id = add_suffix (program_id unfp) "_eq" in
   let hook_eqs _ pm =
@@ -197,7 +197,7 @@ let define_by_eqs ~pm ~poly ~program_mode ~obligations ~tactic ~open_proof opts
   let hook ~pm i p info =
     let () = inline_helpers info in
     let f_cst = match info.term_id with GlobRef.ConstRef c -> c | _ -> assert false in
-    let () = evd := Evd.from_ctx info.term_ustate in
+    let () = evd := Evd.from_ustate info.term_ustate in
     let compiled_info = { program_cst = f_cst;
                           program_split_info = info } in
     progs.(i) <- Some (p, compiled_info);

src/equations_common.ml

@@ -286,7 +286,7 @@ let make_definition ?(check = true) ?opaque ?(poly=PolyFlags.default) evm ?types
     | Some typ -> Vars.universes_of_constr typ
   in
   let used = Univ.Level.Set.union used used' in
-  let evm = Evd.restrict_universe_context evm used in
+  let evm = Evd.restrict_ustate evm used in
   let univs = Evd.univ_entry ~poly evm in
   evm0, evm, Declare.definition_entry ~univs ?types:typ body
 

src/g_equations.mlg

@@ -499,8 +499,9 @@ END
 TACTIC EXTEND is_secvar
 | [ "is_secvar" constr(x) ] ->
    { enter (fun gl ->
+     let env = Proofview.Goal.env gl in
      match kind (Proofview.Goal.sigma gl) x with
-     | Var id when Termops.is_section_variable (Global.env ()) id -> Proofview.tclUNIT ()
+     | Var id when Termops.is_section_variable_env env id -> Proofview.tclUNIT ()
      | _ -> Tacticals.tclFAIL (str "Not a section variable or hypothesis")) }
 END