diff options
| author | Pierre-Marie Pédrot | 2019-12-12 18:44:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-22 14:03:06 +0100 |
| commit | c2341feb58a233598658eeb68a08395b12715b2a (patch) | |
| tree | ba5d4caa869298be94beda0e40767107814954b3 /vernac/vernac.mllib | |
| parent | 1de15982dceaf28740f49f1d6cba61a5473656b0 (diff) | |
Remove the hacks relying on hardwired libobject tags.
The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 5226c2ba65..833c279320 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,11 +19,9 @@ DeclareObl Canonical RecLemmas Library -Prettyp Lemmas Class Auto_ind_decl -Search Indschemes Obligations ComDefinition @@ -31,6 +29,8 @@ Classes ComPrimitive ComAssumption DeclareInd +Search +Prettyp ComInductive ComFixpoint ComProgramFixpoint |