diff options
| author | Pierre-Marie Pédrot | 2018-11-19 19:10:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 19:10:20 +0100 |
| commit | ba8e3caa31e464d1007c4ad54e8d70fd70ca3300 (patch) | |
| tree | f19dd19f84fc0c928e95328f98c8b2a8bf365f27 /plugins/funind | |
| parent | ddbc4215394ecc0845ab29affec2ab27527ee178 (diff) | |
| parent | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (diff) | |
Merge PR #9003: [vernacextend] Consolidate extension points API
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 |