diff options
| author | Emilio Jesus Gallego Arias | 2018-11-14 19:42:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 17:11:51 +0100 |
| commit | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (patch) | |
| tree | 622a359d4d1bc57b104ad042a9b1fc5e5d8d11fd /plugins/funind | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
[vernacextend] Consolidate extension points API
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 155df1c1e0..7e707b423a 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,8 +186,8 @@ VERNAC COMMAND EXTEND Function Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with - | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + | Vernacextend.VtSideff ids, _ when hard -> + Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END @@ -225,7 +225,7 @@ let warning_error names e = VERNAC COMMAND EXTEND NewFunctionalScheme | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater } + => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> { begin @@ -261,7 +261,7 @@ END VERNAC COMMAND EXTEND NewFunctionalCase | ["Functional" "Case" fun_scheme_arg(fas) ] - => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater } + => { Vernacextend.(VtSideff[pi1 fas], VtLater) } -> { Functional_principles_types.build_case_scheme fas } END |