-
Notifications
You must be signed in to change notification settings - Fork 24
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
update meta.yml to be consistent with boilerplate
- Loading branch information
Showing
1 changed file
with
4 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -6,7 +6,7 @@ community: true | |
action: true | ||
plugin: true | ||
doi: 10.4230/LIPIcs.CSL.2012.399 | ||
branch: master | ||
branch: 'master' | ||
|
||
synopsis: Plugin for generating parametricity statements to perform refinement proofs | ||
|
||
|
@@ -59,6 +59,8 @@ namespace: Param | |
|
||
opam-file-maintainer: 'Pierre Roux <[email protected]>' | ||
|
||
opam-file-version: 'dev' | ||
|
||
tested_coq_opam_versions: | ||
- version: 'dev' | ||
|
||
|
@@ -112,7 +114,7 @@ documentation: |- | |
``` | ||
Note that translating a term or module may lead to proof obligations (for some | ||
fixpoints and opaque terms if you did not import `ProofIrrelevence`). You can | ||
fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to | ||
declare a tactic to solve such proof obligations: | ||
```coq | ||
[Global|Local] Parametricity Tactic := <tactic>. | ||
|