Skip to content

Commit

Permalink
Typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlasson
mlasson committed Nov 26, 2016
1 parent 5eba72d commit 0233002
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Readme.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,6 @@ Useful to translate terms containing section variables, or axioms.

Note that all that both translating a term or module may lead to proof obligations (for some fixpoints and opaque terms if you did not import ProofIrrelevence).

- [Global | Local] Parametricity Tactict := t.
- [Global | Local] Parametricity Tactic := t.

Use the tactic t to solve proof obligations generated by the Parametricity command.

0 comments on commit 0233002

Please sign in to comment.