diff options
| author | Gaëtan Gilbert | 2019-10-31 14:55:05 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-31 17:06:15 +0100 |
| commit | 85905b38c15c3d2bb73e878e6e7db180b73d468e (patch) | |
| tree | 715c6f35f099b48aa1c1540d2f53d958b35fe230 /vernac/vernac.mllib | |
| parent | 777109f0068d524ca2a82d405416da273fec3d7f (diff) | |
[prettyp] remove `mod_ops` and `indirect_accessor` parameters
`Prettyp` is now late enough in linking to refer to them.
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7563b4a5d5..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,7 +10,6 @@ Locality Egramml Vernacextend Ppvernac -Prettyp Proof_using Egramcoq Metasyntax @@ -20,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl |