Skip to content
Snippets Groups Projects
Commit 0e607967 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add ssreflect file (from Iris).

parent 2febd0b9
No related branches found
No related tags found
1 merge request!471Add ssreflect file (from Iris).
...@@ -53,6 +53,7 @@ stdpp/nat_cancel.v ...@@ -53,6 +53,7 @@ stdpp/nat_cancel.v
stdpp/namespaces.v stdpp/namespaces.v
stdpp/telescopes.v stdpp/telescopes.v
stdpp/binders.v stdpp/binders.v
stdpp/ssreflect.v
stdpp_unstable/bitblast.v stdpp_unstable/bitblast.v
stdpp_unstable/bitvector.v stdpp_unstable/bitvector.v
......
(** This file provides support for using std++ in combination with the ssreflect
tactics. It patches up some global options of ssreflect. *)
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
From stdpp Require Import options.
(** Restore Coq's normal "if" scope, ssr redefines it. *)
Global Open Scope general_if_scope.
(** See Coq issue #5706 *)
Global Set SsrOldRewriteGoalsOrder.
(** Overwrite ssr's [done] tactic with ours *)
Ltac done := stdpp.tactics.done.
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