aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg16
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_auto.mlg3
-rw-r--r--plugins/ltac/g_ltac.mlg13
-rw-r--r--plugins/ltac/g_tactic.mlg64
-rw-r--r--plugins/ltac/tacinterp.ml12
6 files changed, 42 insertions, 68 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5835d75c79..f97c291c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -330,18 +330,10 @@ END
{
let local_test_lpar_id_colon =
- let err () = raise Stream.Failure in
- Pcoq.Entry.of_parser "lpar_id_colon"
- (fun _ strm ->
- match Util.stream_nth 0 strm with
- | Tok.KEYWORD "(" ->
- (match Util.stream_nth 1 strm with
- | Tok.IDENT _ ->
- (match Util.stream_nth 2 strm with
- | Tok.KEYWORD ":" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_colon" begin
+ lk_kw "(" >> lk_ident >> lk_kw ":"
+ end
let pr_lpar_id_colon _ _ _ _ = mt ()
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 513f5ca77b..d0c94e7903 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -670,7 +670,7 @@ let hResolve id c occ t =
Pretyping.understand env sigma t_hole
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
in
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 8344f9dae3..82c64a9857 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,7 +114,7 @@ END
(** Eauto *)
-TACTIC EXTEND prolog
+TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
{ Eauto.prolog_tac (eval_uconstrs ist l) n }
END
@@ -253,4 +253,3 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
(match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
-
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7ea843ca69..c163438718 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -20,7 +20,6 @@ open Tacexpr
open Namegen
open Genarg
open Genredexpr
-open Tok (* necessary for camlp5 *)
open Names
open Attributes
@@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
- Pcoq.Entry.of_parser "test_bracket_ident"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "[" ->
- (match stream_nth 1 strm with
- | IDENT _ -> ()
- | _ -> raise Stream.Failure)
- | _ -> raise Stream.Failure)
+ let open Pcoq.Lookahead in
+ to_entry "test_bracket_ident" begin
+ lk_kw "[" >> lk_ident
+ end
(* Tactics grammar rules *)
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index f0d6258cd1..8e1e5559af 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -38,45 +38,24 @@ let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)" *)
let test_lpar_id_coloneq =
- Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ ->
- (match stream_nth 2 strm with
- | KEYWORD ":=" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_coloneq" begin
+ lk_kw "(" >> lk_ident >> lk_kw ":="
+ end
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
- Pcoq.Entry.of_parser "lpar_id_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ ->
- (match stream_nth 2 strm with
- | KEYWORD ")" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lpar_id_coloneq" begin
+ lk_kw "(" >> lk_ident >> lk_kw ")"
+ end
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
- Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD "(" ->
- (match stream_nth 1 strm with
- | IDENT _ | NUMERAL _ ->
- (match stream_nth 2 strm with
- | KEYWORD ":=" -> ()
- | _ -> err ())
- | _ -> err ())
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "test_lpar_idnum_coloneq" begin
+ lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
+ end
(* idem for (x:t) *)
open Extraargs
@@ -107,11 +86,10 @@ let check_for_coloneq =
| _ -> err ())
let lookup_at_as_comma =
- Pcoq.Entry.of_parser "lookup_at_as_comma"
- (fun _ strm ->
- match stream_nth 0 strm with
- | KEYWORD (","|"at"|"as") -> ()
- | _ -> err ())
+ let open Pcoq.Lookahead in
+ to_entry "lookup_at_as_comma" begin
+ lk_kws [",";"at";"as"]
+ end
open Constr
open Prim
@@ -611,6 +589,16 @@ GRAMMAR EXTEND Gram
{ TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
| IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
{ TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
+
+ (* Alternative syntax for "pose proof c as id by tac" *)
+ | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":=";
+ c = lconstr; ")" ->
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+ | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":=";
+ c = lconstr; ")" ->
+ { let { CAst.loc = loc; v = id } = lid in
+ TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
{ TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) }
| IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6e620b71db..1d7fe335d1 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) =
let catch_error call_trace f x =
try f x
with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- catching_error call_trace iraise e
+ let e = Exninfo.capture e in
+ catching_error call_trace Exninfo.iraise e
let wrap_error tac k =
if is_traced () then Proofview.tclORELSE tac k else tac
@@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function
try
f ist env sigma c
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
- iraise reraise
+ Exninfo.iraise reraise
(* Interprets a constr expression possibly to first evaluate *)
let interp_constr_may_eval ist env sigma c =
@@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c =
try
interp_may_eval interp_constr ist env sigma c
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term"));
- iraise reraise
+ Exninfo.iraise reraise
in
begin
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:01:57 +0000