Skip to content
Snippets Groups Projects

Add ssreflect file (from Iris).

Merged Robbert Krebbers requested to merge robbert/ssreflect into master
All threads resolved!
2 files
+ 15
0
Compare changes
  • Side-by-side
  • Inline
Files
2
stdpp/ssreflect.v 0 → 100644
+ 14
0
(** 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.
Loading