File: proofmode.v

package info (click to toggle)
coq-iris 4.3.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 4,116 kB
  • sloc: python: 130; makefile: 61; sh: 28; sed: 2
file content (12 lines) | stat: -rw-r--r-- 660 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
 
(** The main proofmode file that everyone should import.
Unless you are working with the guts of the proofmode, do not import any other
file from this folder! *)
From iris.proofmode Require Export ltac_tactics.
(* This [Require Import] is not a no-op: it exports typeclass instances from
these files. *)
From iris.proofmode Require Import class_instances class_instances_later
  class_instances_updates class_instances_embedding
  class_instances_plainly class_instances_internal_eq.
From iris.proofmode Require Import class_instances_frame class_instances_make.
From iris.proofmode Require Import modality_instances.
From iris.prelude Require Import options.