aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/g_indfun.mlg1
-rw-r--r--plugins/funind/plugin_base.dune1
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg1
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg10
-rw-r--r--plugins/ltac/plugin_base.dune1
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ssr/ssrcommon.ml6
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrelim.ml4
-rw-r--r--plugins/ssr/ssrparser.mlg28
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg3
-rw-r--r--plugins/ssrmatching/plugin_base.dune1
-rw-r--r--plugins/ssrmatching/ssrmatching.mli4
18 files changed, 33 insertions, 42 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 92fa94d6dc..ef1d1af199 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -131,8 +131,7 @@ let finish_proof dynamic_infos g =
g
-let refine c =
- Tacmach.refine c
+let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
let thin l = Proofview.V82.of_tactic (Tactics.clear l)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 7e707b423a..8f0440a2a4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -145,7 +145,6 @@ END
{
-module Gram = Pcoq.Gram
module Vernac = Pvernac.Vernac_
module Tactic = Pltac
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 9f583234d8..002eb28eea 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,5 +2,4 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
- (flags :standard -open Gramlib)
(libraries coq.plugins.extraction))
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4c4e51ecc..156ee94a66 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
let local_test_lpar_id_colon =
let err () = raise Stream.Failure in
- Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+ Pcoq.Entry.of_parser "lpar_id_colon"
(fun strm ->
match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" ->
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd8a097154..338839ee96 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -70,7 +70,7 @@ let _ =
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
- Gram.Entry.of_parser "test_bracket_ident"
+ Pcoq.Entry.of_parser "test_bracket_ident"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "[" ->
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index e29f78af5b..ef18dd6cdc 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -45,7 +45,6 @@ let with_tac f tac =
* Subtac. These entries are named Subtac.<foo>
*)
-module Gram = Pcoq.Gram
module Tactic = Pltac
open Pcoq
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2596bc22f2..f7375a0f01 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -226,8 +226,6 @@ let () =
let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
-open Pcoq
-
}
GRAMMAR EXTEND Gram
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 0ce0fbd0cd..46ea3819ac 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -39,7 +39,7 @@ 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 =
- Gram.Entry.of_parser "lpar_id_coloneq"
+ Pcoq.Entry.of_parser "lpar_id_coloneq"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
@@ -53,7 +53,7 @@ let test_lpar_id_coloneq =
(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
- Gram.Entry.of_parser "lpar_id_coloneq"
+ Pcoq.Entry.of_parser "lpar_id_coloneq"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
@@ -67,7 +67,7 @@ let test_lpar_id_rpar =
(* idem for (x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
- Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+ Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD "(" ->
@@ -84,7 +84,7 @@ open Extraargs
(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
let check_for_coloneq =
- Gram.Entry.of_parser "lpar_id_colon"
+ Pcoq.Entry.of_parser "lpar_id_colon"
(fun strm ->
let rec skip_to_rpar p n =
match List.last (Stream.npeek n strm) with
@@ -108,7 +108,7 @@ let check_for_coloneq =
| _ -> err ())
let lookup_at_as_comma =
- Gram.Entry.of_parser "lookup_at_as_comma"
+ Pcoq.Entry.of_parser "lookup_at_as_comma"
(fun strm ->
match stream_nth 0 strm with
| KEYWORD (","|"at"|"as") -> ()
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 1b31655310..5611f5ba16 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,7 +3,6 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
- (flags :standard -open Gramlib)
(libraries coq.stm))
(library
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 188d5de7de..ac2d88dec2 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -697,7 +697,7 @@ type ('b, 'c) argument_interp =
| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
| ArgInterpLegacy :
- (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+ (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
type ('a, 'b, 'c) tactic_argument = {
arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 79f9e093fb..309db539d0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -125,7 +125,7 @@ type ('b, 'c) argument_interp =
| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
| ArgInterpLegacy :
- (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+ (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
type ('a, 'b, 'c) tactic_argument = {
arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index fa58a1c39a..efc4a2c743 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
| _ -> assert false
in loop sigma t [] n in
pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
- Tacmach.refine_no_check t gl
+ Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
@@ -1092,8 +1092,8 @@ let tclDO n tac =
let _, info = CErrors.push e in
let e' = CErrors.UserError (l, prefix i ++ s) in
Util.iraise (e', info)
- | Ploc.Exc(loc, CErrors.UserError (l, s)) ->
- raise (Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+ | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) ->
+ raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
let rec loop i gl =
if i = n then tac_err_at i gl else
(tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e92489e568..e25c93bf0a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm
val mk_ast_closure_term :
[ `None | `Parens | `DoubleParens | `At ] ->
Constrexpr.constr_expr -> ast_closure_term
-val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal
+val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal
Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term
val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d09b81593e..2c9ec3a7cf 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -398,13 +398,13 @@ let revtoptac n0 gl =
let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
- refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl
+ Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
let equality_inj l b id c gl =
let msg = ref "" in
try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
with
- | Ploc.Exc(_,CErrors.UserError (_,s))
+ | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
| CErrors.UserError (_,s)
when msg := Pp.string_of_ppcmds s;
!msg = "Not a projectable equality but a discriminable one." ||
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7c91860228..2dff0cc84f 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -268,16 +268,16 @@ let negate_parser f x =
| Some _ -> raise Stream.Failure
let test_not_ssrslashnum =
- Pcoq.Gram.Entry.of_parser
+ Pcoq.Entry.of_parser
"test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
let test_ssrslashnum00 =
- Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
let test_ssrslashnum10 =
- Pcoq.Gram.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+ Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
let test_ssrslashnum11 =
- Pcoq.Gram.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+ Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
let test_ssrslashnum01 =
- Pcoq.Gram.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+ Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
}
@@ -470,7 +470,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
@@ -481,7 +481,7 @@ let input_term_annotation strm =
| Tok.KEYWORD "@" :: _ -> `At
| _ -> `None
let term_annotation =
- Gram.Entry.of_parser "term_annotation" input_term_annotation
+ Pcoq.Entry.of_parser "term_annotation" input_term_annotation
(* terms *)
@@ -800,7 +800,7 @@ let reject_ssrhid strm =
| _ -> ())
| _ -> ()
-let test_nohidden = Pcoq.Gram.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
}
@@ -961,7 +961,7 @@ let accept_ssrfwdid strm =
| Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
| _ -> raise Stream.Failure
-let test_ssrfwdid = Gram.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
+let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid
}
@@ -1540,7 +1540,7 @@ let accept_ssrseqvar strm =
accept_before_syms_or_ids ["["] ["first";"last"] strm
| _ -> raise Stream.Failure
-let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
+let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar
let swaptacarg (loc, b) = (b, []), Some (TacId [])
@@ -1628,7 +1628,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
}
@@ -1955,7 +1955,7 @@ let accept_ssreqid strm =
accept_before_syms [":"] strm
| _ -> raise Stream.Failure
-let test_ssreqid = Gram.Entry.of_parser "test_ssreqid" accept_ssreqid
+let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
}
@@ -2373,7 +2373,7 @@ let test_ssr_rw_syntax =
match Util.stream_nth 0 strm with
| Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
| _ -> raise Stream.Failure in
- Gram.Entry.of_parser "test_ssr_rw_syntax" test
+ Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
}
@@ -2583,7 +2583,7 @@ let accept_idcomma strm =
| Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
| _ -> raise Stream.Failure
-let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma
+let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma
}
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 3f0794fdd4..4ddaeb49fd 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -11,7 +11,6 @@
{
open Ltac_plugin
-open Pcoq
open Pcoq.Constr
open Ssrmatching
open Ssrmatching.Internal
@@ -69,7 +68,7 @@ let input_ssrtermkind strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> '('
| Tok.KEYWORD "@" -> '@'
| _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
}
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
index 1450a94de1..06f67c3774 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -2,5 +2,4 @@
(name ssrmatching_plugin)
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
- (flags :standard -open Gramlib)
(libraries coq.plugins.ltac))
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 63b7e1783e..93a8c48435 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -230,7 +230,7 @@ sig
val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type
val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern
val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern
- val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
+ val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
val pr_rpattern : rpattern -> Pp.t
val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
@@ -238,7 +238,7 @@ sig
val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
- val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
+ val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
val pr_ssrterm : cpattern -> Pp.t
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:54:31 +0000