Commit d9e55d3d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/no-global' into 'master'

remove a Global Arguments Pos.of_nat from the middle of a proof

See merge request iris/stdpp!350
parents e6194e28 df9b4add
......@@ -13,6 +13,7 @@ Coq 8.10 is no longer supported by this release.
- Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
- Rename `Is_true_false``Is_true_false_2` and `eq_None_ne_Some``eq_None_ne_Some_1`.
- Rename `decide_iff``decide_ext` and `bool_decide_iff``bool_decide_ext`.
- Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
......@@ -19,7 +19,6 @@ Program Definition finite_countable `{Finite A} : Countable A := {|
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
Global Arguments Pos.of_nat : simpl never.
Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
......
Supports Markdown
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