Skip to content
Snippets Groups Projects
Commit ba8d07ed authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'fix-typos' into 'master'

Fix some typos in docs

See merge request iris/iris!433
parents 6dba682d a4d6d913
No related branches found
No related tags found
No related merge requests found
......@@ -91,7 +91,7 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
(** The [FromModal M sel P Q] class is used by the [iModIntro] tactic to transform
a goal [P] into a modality [M] and proposition [Q].
The inputs are [P] and [sel] and the outputs are [M] and [Q].
......
......@@ -818,8 +818,8 @@ Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
transform_intuitionistic_env_dom i : Γin !! i = None Γout !! i = None;
}.
(* The class [TransformIntuitionisticEnv M C Γin Γout filtered] is used to transform
the intuitionistic environment using a type class [C].
(* The class [TransformSpatialEnv M C Γin Γout filtered] is used to transform
the spatial environment using a type class [C].
Inputs:
- [Γin] : the original environment.
......
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