aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.ml411
-rw-r--r--plugins/firstorder/ground.ml9
-rw-r--r--plugins/firstorder/instances.ml32
-rw-r--r--plugins/firstorder/rules.ml32
4 files changed, 40 insertions, 44 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index bbb9feae2..e3fab6d01 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,7 +15,6 @@ open Ground
open Goptions
open Tacmach.New
open Tacticals.New
-open Proofview.Notations
open Tacinterp
open Libnames
open Stdarg
@@ -84,24 +83,24 @@ let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
let gen_ground_tac flag taco ids bases =
let backup= !qflag in
Proofview.tclOR begin
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
qflag:=flag;
let solver=
match taco with
Some tac-> tac
| None-> snd (default_solver ()) in
let startseq k =
- Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let seq=empty_seq !ground_depth in
let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
- Sigma.Unsafe.of_pair (k seq, sigma)
- end }
+ tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
+ end
in
let result=ground_tac solver startseq in
qflag := backup;
result
- end }
+ end
end
(fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index ab1dd07c1..0fa3089e7 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -14,7 +14,6 @@ open Instances
open Term
open Tacmach.New
open Tacticals.New
-open Proofview.Notations
let update_flags ()=
let predref=ref Names.Cpred.empty in
@@ -31,10 +30,10 @@ let update_flags ()=
(Names.Id.Pred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
update_flags ();
let rec toptac skipped seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let () =
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then
@@ -127,7 +126,7 @@ let ground_tac solver startseq =
end
with Heap.EmptyHeap->solver
end
- end } in
+ end in
let n = List.length (Proofview.Goal.hyps gl) in
startseq (fun seq -> wrap n true (toptac []) seq)
- end }
+ end
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 04bca584f..e1d765a42 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Formula
open Sequent
open Names
open Misctypes
-open Sigma.Notations
open Context.Rel.Declaration
let compare_instance inst1 inst2=
@@ -114,9 +113,7 @@ let mk_open_instance env evmap id idc m t =
let rec aux n avoid env evmap decls =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id_in_env avoid var_id env) in
- let evmap = Sigma.Unsafe.of_evar_map evmap in
- let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
- let evmap = Sigma.to_evar_map evmap in
+ let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
let decl = LocalAssum (Name nid, c) in
aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
@@ -126,7 +123,7 @@ let mk_open_instance env evmap id idc m t =
let left_instance_tac (inst,id) continue seq=
let open EConstr in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
match inst with
Phantom dom->
@@ -137,10 +134,10 @@ let left_instance_tac (inst,id) continue seq=
[tclTHENLIST
[introf;
(pf_constr_of_global id >>= fun idc ->
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let id0 = List.nth (pf_ids_of_hyps gl) 0 in
generalize [mkApp(idc, [|mkVar id0|])]
- end });
+ end);
introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -153,7 +150,7 @@ let left_instance_tac (inst,id) continue seq=
let special_generalize=
if m>0 then
(pf_constr_of_global id >>= fun idc ->
- Proofview.Goal.s_enter { s_enter = begin fun gl->
+ Proofview.Goal.enter begin fun gl->
let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
let gt=
it_mkLambda_or_LetIn
@@ -162,8 +159,9 @@ let left_instance_tac (inst,id) continue seq=
try Typing.type_of (pf_env gl) evmap gt
with e when CErrors.noncritical e ->
user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
- Sigma.Unsafe.of_pair (generalize [gt], evmap)
- end })
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
+ (generalize [gt])
+ end)
else
pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
in
@@ -172,20 +170,20 @@ let left_instance_tac (inst,id) continue seq=
introf;
tclSOLVE
[wrap 1 false continue (deepen (record (id,Some c) seq))]]
- end }
+ end
let right_instance_tac inst continue seq=
let open EConstr in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
match inst with
Phantom dom ->
tclTHENS (cut dom)
[tclTHENLIST
[introf;
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let id0 = List.nth (pf_ids_of_hyps gl) 0 in
split (ImplicitBindings [mkVar id0])
- end };
+ end;
tclSOLVE [wrap 0 true continue (deepen seq)]];
tclTRY assumption]
| Real ((0,t),_) ->
@@ -193,7 +191,7 @@ let right_instance_tac inst continue seq=
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 (Pp.str "not implemented ... yet")
- end }
+ end
let instance_tac inst=
if (snd inst)==dummy_id then
@@ -202,9 +200,9 @@ let instance_tac inst=
left_instance_tac inst
let quantified_tac lf backtrack continue seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let insts=give_instances (project gl) lf seq in
tclORELSE
(tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
backtrack
- end }
+ end
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f745dbeb4..b7fe25a32 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -32,7 +32,7 @@ type lseqtac= global_reference -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq =
- Proofview.Goal.nf_enter { enter = begin fun gls ->
+ Proofview.Goal.nf_enter begin fun gls ->
Control.check_for_interrupt ();
let nc = Proofview.Goal.hyps gls in
let env=pf_env gls in
@@ -52,7 +52,7 @@ let wrap n b continue seq =
let seq2=if b then
add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
continue seq2
- end }
+ end
let basename_of_global=function
VarRef id->id
@@ -65,12 +65,12 @@ let clear_global=function
(* connection rules *)
let axiom_tac t seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
try
pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
exact_no_check c
with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
- end }
+ end
let ll_atom_tac a backtrack id continue seq =
let open EConstr in
@@ -107,7 +107,7 @@ let arrow_tac backtrack continue seq=
(* left connectives rules *)
let left_and_tac ind backtrack id continue seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let n=(construct_nhyps (pf_env gl) ind).(0) in
tclIFTHENELSE
(tclTHENLIST
@@ -116,10 +116,10 @@ let left_and_tac ind backtrack id continue seq =
tclDO n intro])
(wrap n false continue seq)
backtrack
- end }
+ end
let left_or_tac ind backtrack id continue seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let v=construct_nhyps (pf_env gl) ind in
let f n=
tclTHENLIST
@@ -130,7 +130,7 @@ let left_or_tac ind backtrack id continue seq =
(pf_constr_of_global id >>= simplest_elim)
(Array.map f v)
backtrack
- end }
+ end
let left_false_tac id=
Tacticals.New.pf_constr_of_global id >>= simplest_elim
@@ -140,7 +140,7 @@ let left_false_tac id=
(* We use this function for false, and, or, exists *)
let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in
let vargs=Array.of_list largs in
(* construire le terme H->B, le generaliser etc *)
@@ -161,7 +161,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
clear_global id;
tclDO lp intro])
(wrap lp false continue seq) backtrack
- end }
+ end
let ll_arrow_tac a b c backtrack id continue seq=
let open EConstr in
@@ -199,7 +199,7 @@ let forall_tac backtrack continue seq=
backtrack)
let left_exists_tac ind backtrack id continue seq =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let n=(construct_nhyps (pf_env gl) ind).(0) in
tclIFTHENELSE
(Tacticals.New.pf_constr_of_global id >>= simplest_elim)
@@ -207,7 +207,7 @@ let left_exists_tac ind backtrack id continue seq =
tclDO n intro;
(wrap (n-1) false continue seq)])
backtrack
- end }
+ end
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
@@ -215,12 +215,12 @@ let ll_forall_tac prod backtrack id continue seq=
[tclTHENLIST
[intro;
(pf_constr_of_global id >>= fun idc ->
- Proofview.Goal.enter { enter = begin fun gls->
+ Proofview.Goal.enter begin fun gls->
let open EConstr in
let id0 = List.nth (pf_ids_of_hyps gls) 0 in
let term=mkApp(idc,[|mkVar(id0)|]) in
tclTHEN (generalize [term]) (clear [id0])
- end });
+ end);
clear_global id;
intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -239,9 +239,9 @@ let defined_connectives=lazy
AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
let normalize_evaluables=
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
unfold_in_concl (Lazy.force defined_connectives) <*>
tclMAP
(fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
(pf_ids_of_hyps gl)
- end }
+ end
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 12:06:44 +0000