Commit e3027f8d authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of fix/cofix without a name; these are deprecated in Coq 8.8.

parent a85ee3f5
......@@ -348,11 +348,11 @@ Fixpoint gen_tree_of_list {T}
Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) :
gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
Proof.
revert t k l; fix 1; intros [|n ts] k l; simpl; auto.
revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto.
trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
- rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
rewrite reverse_cons, <-!(assoc_L _), gen_tree_of_to_list; simpl; auto.
rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
- simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
by (by rewrite reverse_length).
Qed.
......
......@@ -48,11 +48,11 @@ Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
Proof.
assert ( x y (p : x y) y' (q : x y'),
y = y' eq_dep nat (le x) y p y' q) as aux.
{ fix 3. intros x ? [|y p] ? [|y' q].
{ fix FIX 3. intros x ? [|y p] ? [|y' q].
- done.
- clear nat_le_pi. intros; exfalso; auto with lia.
- clear nat_le_pi. intros; exfalso; auto with lia.
- injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
- clear FIX. intros; exfalso; auto with lia.
- clear FIX. intros; exfalso; auto with lia.
- injection 1. intros Hy. by case (FIX x y p y' q Hy). }
intros x y p q.
by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed.
......
......@@ -25,7 +25,7 @@ Proof. done. Qed.
Lemma pretty_N_go_help_irrel x acc1 acc2 s :
pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
Proof.
revert x acc1 acc2 s; fix 2; intros x [acc1] [acc2] s; simpl.
revert x acc1 acc2 s; fix FIX 2; intros x [acc1] [acc2] s; simpl.
destruct (decide (0 < x)%N); auto.
Qed.
Lemma pretty_N_go_step x s :
......
......@@ -223,7 +223,7 @@ Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x)
( y Hy Hy', E _ (f y Hy) (g y Hy')) E _ (F x f) (F x g))
(x : A) (acc1 acc2 : Acc R x) :
E _ (Fix_F B F acc1) (Fix_F B F acc2).
Proof. revert x acc1 acc2. fix 2. intros x [acc1] [acc2]; simpl; auto. Qed.
Proof. revert x acc1 acc2. fix FIX 2. intros x [acc1] [acc2]; simpl; auto. Qed.
Lemma Fix_unfold_rel `{R: relation A} (wfR: wf R) (B: A Type) (E: x, relation (B x))
(F: x, ( y, R y x B y) B x)
......
......@@ -41,9 +41,9 @@ Proof. by constructor. Qed.
Global Instance equal_equivalence : Equivalence (@{stream A}).
Proof.
split.
- now cofix; intros [??]; constructor.
- now cofix; intros ?? [??]; constructor.
- cofix; intros ??? [??] [??]; constructor; etrans; eauto.
- now cofix FIX; intros [??]; constructor.
- now cofix FIX; intros ?? [??]; constructor.
- cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
Qed.
Global Instance scons_proper x : Proper (() ==> ()) (scons x).
Proof. by constructor. Qed.
......
......@@ -45,7 +45,7 @@ Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None.
Proof.
unfold fresh_string. destruct (m !! s) as [a|] eqn:Hs; [clear a Hs|done].
generalize 0 (wf_guard 32 (fresh_string_R_wf s m) 0); revert m.
fix 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
fix FIX 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
destruct (Some_dec (m !! _)) as [[??]|?]; auto.
Qed.
Definition fresh_string_of_set (s : string) (X : stringset) : string :=
......
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