File tree 1 file changed +4
-2
lines changed
1 file changed +4
-2
lines changed Original file line number Diff line number Diff line change @@ -6,7 +6,7 @@ community: true
6
6
action : true
7
7
plugin : true
8
8
doi : 10.4230/LIPIcs.CSL.2012.399
9
- branch : master
9
+ branch : ' master'
10
10
11
11
synopsis : Plugin for generating parametricity statements to perform refinement proofs
12
12
@@ -59,6 +59,8 @@ namespace: Param
59
59
60
60
opam-file-maintainer : ' Pierre Roux <pierre.roux@onera.fr>'
61
61
62
+ opam-file-version : ' dev'
63
+
62
64
tested_coq_opam_versions :
63
65
- version : ' dev'
64
66
@@ -112,7 +114,7 @@ documentation: |-
112
114
```
113
115
114
116
Note that translating a term or module may lead to proof obligations (for some
115
- fixpoints and opaque terms if you did not import `ProofIrrelevence`). You can
117
+ fixpoints and opaque terms if you did not import `ProofIrrelevence`). You need to
116
118
declare a tactic to solve such proof obligations:
117
119
```coq
118
120
[Global|Local] Parametricity Tactic := <tactic>.
You can’t perform that action at this time.
0 commit comments