diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/dune | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 25 |
2 files changed, 21 insertions, 8 deletions
diff --git a/plugins/funind/dune b/plugins/funind/dune index e594ffbd02..42377f37f4 100644 --- a/plugins/funind/dune +++ b/plugins/funind/dune @@ -1,7 +1,7 @@ (library (name recdef_plugin) - (public_name coq.plugins.funind) + (public_name coq-core.plugins.funind) (synopsis "Coq's functional induction plugin") - (libraries coq.plugins.extraction)) + (libraries coq-core.plugins.extraction)) (coq.pp (modules g_indfun)) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index ca6ae150a7..15cf88f827 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -195,16 +195,29 @@ let is_interactive recsl = } +(* For usability we temporarily switch off some flags during the call + to Function. However this is not satisfactory: + + 1- Function should not warn "non-recursive" and call the Definition + mechanism instead of Fixpoint when needed + + 2- Only for automatically generated names should + unused-pattern-matching-variable be ignored. *) + VERNAC COMMAND EXTEND Function STATE CUSTOM | ["Function" ne_function_fix_definition_list_sep(recsl,"with")] => { classify_funind recsl } -> { - if is_interactive recsl then - Vernacextend.VtOpenProof (fun () -> - Gen_principle.do_generate_principle_interactive (List.map snd recsl)) - else - Vernacextend.VtDefault (fun () -> - Gen_principle.do_generate_principle (List.map snd recsl)) } + let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in + if is_interactive recsl then + Vernacextend.VtOpenProof (fun () -> + CWarnings.with_warn warn + Gen_principle.do_generate_principle_interactive (List.map snd recsl)) + else + Vernacextend.VtDefault (fun () -> + CWarnings.with_warn warn + Gen_principle.do_generate_principle (List.map snd recsl)) + } END { |