Skip to content
Snippets Groups Projects
Commit a7a63cf8 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'robbert/ssreflect' into 'master'

Update prelude file to use new ssreflect file from std++.

See merge request iris/iris!917
parents 8c4c3b74 aa4b0596
No related branches found
No related tags found
No related merge requests found
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
From stdpp Require Export ssreflect.
From iris.prelude Require Import options.
Global Open Scope general_if_scope.
Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
(** Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12, which Iris depends on. *)
Global Hint Mode Equiv ! : typeclass_instances.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment