aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/firstorder/rules.ml2
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extratactics.ml44
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml8
-rw-r--r--plugins/omega/coq_omega.ml12
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrparser.ml42
11 files changed, 25 insertions, 25 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index c2bc8c079c..b0f97c59b8 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -224,7 +224,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let eq = Lazy.force eq in
let concl = EConstr.Unsafe.to_constr concl in
@@ -240,7 +240,7 @@ module Btauto = struct
end
let tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let concl = EConstr.Unsafe.to_constr concl in
let sigma = Tacmach.New.project gl in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b13580bc03..3ae777cc9a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq =
- Proofview.Goal.nf_enter begin fun gls ->
+ Proofview.Goal.enter begin fun gls ->
Control.check_for_interrupt ();
let nc = Proofview.Goal.hyps gls in
let env=pf_env gls in
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 73490a2dfd..b0277e9cc2 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -99,7 +99,7 @@ let let_evar name typ =
let hget_evar n =
let open EConstr in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let evl = evar_list sigma concl in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d42876e23e..ba3fa6fa0d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -781,9 +781,9 @@ END
(**********************************************************************)
TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
END
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 414173ca79..67ffae59cc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1469,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
independently of goals. *)
and interp_genarg_constr_list ist x =
- Ftactic.nf_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
@@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1696,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInductionDestruct (isrec,ev,(l,el)) ->
(* spiwack: some unknown part of destruct needs the goal to be
prenormalised. *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
@@ -1723,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Conversion *)
| TacReduce (r,cl) ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 105b5c59ae..48d677a864 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -58,7 +58,7 @@ let db_pr_goal gl =
str" " ++ pc) ++ fnl ()
let db_pr_goal =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let pg = db_pr_goal gl in
Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
end
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f22147f8b0..e0a369ca5f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
let vm = dump_varmap (spec.typ) (vm_of_list env) in
(* todo : directly generate the proof term - or generalize before conversion? *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclTHENLIST
[
Tactics.change_concl
@@ -1709,7 +1709,7 @@ let micromega_gen
(normalise:'cst atom -> 'cst mc_cnf)
unsat deduce
spec dumpexpr prover tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Tacmach.New.pf_concl gl in
let hyps = Tacmach.New.pf_hyps_types gl in
@@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff =
let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
let vm = dump_varmap (typ) (vm_of_list env) in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclTHENLIST
[
(Tactics.change_concl
@@ -1817,7 +1817,7 @@ let micromega_genr prover tac =
proof_typ = Lazy.force coq_QWitness ;
dump_proof = dump_psatz coq_Q dump_q
} in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Tacmach.New.pf_concl gl in
let hyps = Tacmach.New.pf_hyps_types gl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e14c4e2ec1..abae6940fa 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -588,7 +588,7 @@ let abstract_path sigma typ path t =
let focused_simpl path =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
convert_concl_no_check newc DEFAULTcast
end
@@ -656,7 +656,7 @@ let new_hole env sigma c =
let clever_rewrite_base_poly typ p result theorem =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let full = pf_concl gl in
let env = pf_env gl in
let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
@@ -708,7 +708,7 @@ let refine_app gl t =
let clever_rewrite p vpath t =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let full = pf_concl gl in
let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
@@ -1763,7 +1763,7 @@ let onClearedName id tac =
(* so renaming may be necessary *)
tclTHEN
(tclTRY (clear [id]))
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let id = fresh_id Id.Set.empty id gl in
tclTHEN (introduction id) (tac id)
end)
@@ -1771,7 +1771,7 @@ let onClearedName id tac =
let onClearedName2 id tac =
tclTHEN
(tclTRY (clear [id]))
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in
tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
@@ -1956,7 +1956,7 @@ let destructure_goal =
try
let dec = decidability t in
tclTHEN
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
end)
intro
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e603480656..930048400a 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1049,7 +1049,7 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
Tactics.apply (Lazy.force coq_I)
let total_reflexive_omega_tactic unsafe =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Coqlib.check_required_library ["Coq";"romega";"ROmega"];
rst_omega_eq ();
rst_omega_var ();
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f3c758e5c..f2f236f448 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
(** Basic tactics *)
-let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl ->
+let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
match EConstr.kind (Proofview.Goal.sigma gl) concl with
| Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 8b9c94f2db..a7aae5bd31 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
END
let vmexacttac pf =
- Goal.nf_enter begin fun gl ->
+ Goal.enter begin fun gl ->
exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:29:22 +0000