aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.ml410
-rw-r--r--plugins/firstorder/ground.ml2
-rw-r--r--plugins/firstorder/ground_plugin.mlpack (renamed from plugins/firstorder/ground_plugin.mllib)1
-rw-r--r--plugins/firstorder/instances.ml11
-rw-r--r--plugins/firstorder/rules.ml14
5 files changed, 20 insertions, 18 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3e8be36993..cec3505a97 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,9 @@ open Goptions
open Tacticals
open Tacinterp
open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
DECLARE PLUGIN "ground_plugin"
@@ -71,7 +74,7 @@ END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
| [ "Print" "Firstorder" "Solver" ] -> [
- Pp.msg_info
+ Feedback.msg_info
(Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
END
@@ -118,6 +121,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
ARGUMENT EXTEND firstorder_using
+ TYPED AS reference_list
PRINTED BY pr_firstorder_using_typed
RAW_TYPED AS reference_list
RAW_PRINTED BY pr_firstorder_using_raw
@@ -127,7 +131,7 @@ ARGUMENT EXTEND firstorder_using
| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
| [ "using" reference(a) reference(b) reference_list(l) ] -> [
Flags.if_verbose
- Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+ Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
a::b::l
]
| [ ] -> [ [] ]
@@ -149,6 +153,8 @@ TACTIC EXTEND gintuition
END
open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
let default_declarative_automation =
Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 3b9f67f664..d7da85b4f4 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -32,7 +32,7 @@ let ground_tac solver startseq gl=
update_flags ();
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
- then Pp.msg_debug (Printer.pr_goal gl);
+ then Feedback.msg_debug (Printer.pr_goal gl);
tclORELSE (axiom_tac seq.gl seq)
begin
try
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack
index 447a1fb513..65fb2e9a1d 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mlpack
@@ -5,4 +5,3 @@ Rules
Instances
Ground
G_ground
-Ground_plugin_mod
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0bc40136c5..5eff2f2774 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -12,7 +12,6 @@ open Errors
open Util
open Term
open Vars
-open Glob_term
open Tacmach
open Tactics
open Tacticals
@@ -98,8 +97,6 @@ let rec collect_quantified seq=
(* open instances processor *)
-let dummy_constr=mkMeta (-1)
-
let dummy_bvid=Id.of_string "x"
let mk_open_instance id idc gl m t=
@@ -138,9 +135,9 @@ let left_instance_tac (inst,id) continue seq=
[tclTHENLIST
[Proofview.V82.of_tactic introf;
pf_constr_of_global id (fun idc ->
- (fun gls->generalize
+ (fun gls-> Proofview.V82.of_tactic (generalize
[mkApp(idc,
- [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
+ [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -161,10 +158,10 @@ let left_instance_tac (inst,id) continue seq=
try Typing.type_of (pf_env gl) evmap gt
with e when Errors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
- tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
+ tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
else
pf_constr_of_global id (fun idc ->
- generalize [mkApp(idc,[|t|])])
+ Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
in
tclTHENLIST
[special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index c05015c538..92b6e828e8 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -52,13 +52,13 @@ let basename_of_global=function
| _->assert false
let clear_global=function
- VarRef id->clear [id]
+ VarRef id-> Proofview.V82.of_tactic (clear [id])
| _->tclIDTAC
(* connection rules *)
let axiom_tac t seq=
- try pf_constr_of_global (find_left t seq) exact_no_check
+ try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
@@ -67,7 +67,7 @@ let ll_atom_tac a backtrack id continue seq=
tclTHENLIST
[pf_constr_of_global (find_left a seq) (fun left ->
pf_constr_of_global id (fun id ->
- generalize [mkApp(id, [|left|])]));
+ Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -135,7 +135,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
(tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
clear_global id;
tclDO lp (Proofview.V82.of_tactic intro)])
(wrap lp false continue seq) backtrack gl
@@ -151,9 +151,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
clear_global id;
wrap 1 false continue seq];
tclTHENS (Proofview.V82.of_tactic (cut cc))
- [pf_constr_of_global id exact_no_check;
+ [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
tclTHENLIST
- [pf_constr_of_global id (fun idc -> generalize [d idc]);
+ [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
clear_global id;
Proofview.V82.of_tactic introf;
Proofview.V82.of_tactic introf;
@@ -192,7 +192,7 @@ let ll_forall_tac prod backtrack id continue seq=
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls));
+ tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
clear_global id;
Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:55:38 +0000