Commit 270ae8c3 authored by MEVEL Glen's avatar MEVEL Glen

update Coq from 8.9.1 to 8.10*

parent 3f4208d3
......@@ -10,6 +10,7 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
"coq-iris" { (= "dev.2020-03-23.0.3a0d7152") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
......@@ -81,6 +81,7 @@ Inductive bin_op : Set :=
| LeOp | LtOp | EqOp. (* Relations *)
Inductive binder := BAnon | BNamed : string binder.
Declare Scope binder_scope.
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
......
......@@ -43,15 +43,15 @@ Ltac inv_head_step :=
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
Local Hint Resolve to_of_val.
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Resolve to_of_val : core.
Global Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
......
......@@ -109,8 +109,8 @@ Record Inv D F K R V : Prop := {
Inv_data : forall x, V x = V (R x)
}.
Hint Resolve is_rdsf_is_dsf.
Hint Resolve Inv_rdsf Inv_incl Inv_data.
Hint Resolve is_rdsf_is_dsf : core.
Hint Resolve Inv_rdsf Inv_incl Inv_data : core.
(* Throughout, we instantiate the parameter [r] of Alstrup et al.'s proof
with the value 1. Thus, we write just [Phi] for [Phi 1]. *)
......
......@@ -112,7 +112,7 @@ Lemma tclosure_intro_right:
forall (A : Type) (R : binary A) y x z,
rtclosure R x y -> R y z -> tclosure R x z.
Proof using.
Hint Constructors tclosure.
Hint Constructors tclosure : core.
introv M N. induction M using rtclosure_ind_l; autos*.
Qed.
......@@ -281,7 +281,7 @@ Qed.
Lemma le_refl : refl Peano.le.
Proof using. intros_all; omega. Qed.
Hint Resolve le_refl.
Hint Resolve le_refl : core.
......
......@@ -178,7 +178,7 @@ Lemma compress_preserves_is_repr_direct':
is_repr F x r ->
is_repr compress x r.
Proof using x_edge_y is_dsf_F y_path_z.
Hint Unfold is_repr.
Hint Unfold is_repr : core.
intros x' r' Rz [Pr' Rr']. split.
{ induction Pr' as [r'|y' x' z'] using rtclosure_ind_l.
{ now constructor. }
......
......@@ -68,7 +68,7 @@ Definition is_rdsf_numerous_family := proj53 is_rdsf_F.
Definition is_rdsf_finite := proj54 is_rdsf_F.
Definition is_rdsf_zero_rank_outside_domain := proj55 is_rdsf_F.
Hint Resolve is_rdsf_is_dsf.
Hint Resolve is_rdsf_is_dsf : core.
Hint Resolve is_rdsf_finite : finite.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment