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

Fix typo.

parent 4b8fabaf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/proofmode.v
+ 1
− 1
View file @ 8c4c3b74
(** The main proofmode file taht everyone should import.
(** 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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment