File: ssreflect.v

package info (click to toggle)
coq-stdpp 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,696 kB
  • sloc: makefile: 52; sh: 35; sed: 1
file content (14 lines) | stat: -rw-r--r-- 490 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
(** 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.