diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/coretactics.mlg | 7 | ||||
| -rw-r--r-- | plugins/ltac/dune | 8 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 15 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 6 |
5 files changed, 9 insertions, 35 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index e39c066c95..b20c4d173d 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } END -(** Double induction *) - -TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () } -| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - { Elim.h_double_induction h1 h2 } -END - (* Admit *) TACTIC EXTEND admit diff --git a/plugins/ltac/dune b/plugins/ltac/dune index 6558ecbfe8..9ec2b10873 100644 --- a/plugins/ltac/dune +++ b/plugins/ltac/dune @@ -1,15 +1,15 @@ (library (name ltac_plugin) - (public_name coq.plugins.ltac) + (public_name coq-core.plugins.ltac) (synopsis "Coq's LTAC tactic language") (modules :standard \ tauto) - (libraries coq.stm)) + (libraries coq-core.stm)) (library (name tauto_plugin) - (public_name coq.plugins.tauto) + (public_name coq-core.plugins.tauto) (synopsis "Coq's tauto tactic") (modules tauto) - (libraries coq.plugins.ltac)) + (libraries coq-core.plugins.ltac)) (coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs)) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 069a342b2a..82b41e41bd 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -11,7 +11,6 @@ { open Pp -open Constr open Stdarg open Pcoq.Prim open Pcoq.Constr @@ -199,20 +198,6 @@ TACTIC EXTEND unify END { -let deprecated_convert_concl_no_check = - CWarnings.create - ~name:"convert_concl_no_check" ~category:"deprecated" - (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.") -} - -TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> { - deprecated_convert_concl_no_check (); - Tactics.convert_concl ~check:false x DEFAULTcast - } -END - -{ let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 6bf330c830..e7902d06eb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program -| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } -| [ "Obligations" ] -> { show_obligations None } +| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) } +| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None } END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program -| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } -| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) } +| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } +| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) } END { diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index aa2449d962..937d579012 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -436,11 +436,7 @@ let finish_timing ~prefix name = (* ******************** *) let print_results_filter ~cutoff ~filter = - (* The STM doesn't provide yet a proper document query and traversal - API, thus we need to re-check if some states are current anymore - (due to backtracking) using the `state_of_id` API. *) - let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in - data := SM.filter valid !data; + data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data; let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in |