aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml1
-rw-r--r--plugins/ssr/ssrequality.ml32
-rw-r--r--plugins/ssr/ssrparser.mlg47
-rw-r--r--plugins/ssr/ssrvernac.mlg1
4 files changed, 41 insertions, 40 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 33e9f871fd..473612fda7 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
-open Decl_kinds
let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index aa1316f15e..4c6b7cdcb6 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -128,10 +128,9 @@ let newssrcongrtac arg ist gl =
x, re_sig si sigma in
let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
let ssr_congr lr = EConstr.mkApp (arr, lr) in
+ let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
(* here the two cases: simple equality or arrow *)
- let equality, _, eq_args, gl' =
- let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
- pf_saturate gl (EConstr.of_constr eq) 3 in
+ let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in
tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
(fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
(fun () ->
@@ -336,17 +335,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
let sigma, p = (* The resulting goal *)
Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
- let elim, gl =
- let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
+ let sigma, elim =
let sort = elimination_sort_of_goal gl in
- let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
- if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
- let elim, _ = destConst elim in
- let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
- let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
- mkConst c1', gl in
- let elim = EConstr.of_constr elim in
+ match Equality.eq_elimination_ref (dir = L2R) sort with
+ | Some r -> Evd.fresh_global env sigma r
+ | None ->
+ let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in
+ let sort = elimination_sort_of_goal gl in
+ let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in
+ if dir = R2L then sigma, elim else
+ let elim, _ = EConstr.destConst sigma elim in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
+ let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
+ let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
+ sigma, EConstr.of_constr (mkConst c1')
+ in
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
(* We check the proof is well typed *)
let sigma, proof_ty =
@@ -491,7 +494,8 @@ let rwprocess_rule dir rule gl =
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
EConstr.mkApp (pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
+ let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in
+ if EConstr.eq_constr sigma a.(0) trty then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 962730d8dc..a1f707ffa8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -32,7 +32,6 @@ open Ppconstr
open Namegen
open Tactypes
-open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -235,7 +234,7 @@ let pr_ssrsimpl _ _ _ = pr_simpl
let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
-let test_ssrslashnum b1 b2 strm =
+let test_ssrslashnum b1 b2 _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
@@ -276,8 +275,8 @@ let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false
-let negate_parser f x =
- let rc = try Some (f x) with Stream.Failure -> None in
+let negate_parser f tok x =
+ let rc = try Some (f tok x) with Stream.Failure -> None in
match rc with
| None -> ()
| Some _ -> raise Stream.Failure
@@ -474,7 +473,7 @@ END
(* Old kinds of terms *)
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> xInParens
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
@@ -483,7 +482,7 @@ let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
-let input_term_annotation strm =
+let input_term_annotation _ strm =
match Stream.npeek 2 strm with
| Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
| Tok.KEYWORD "(" :: _ -> `Parens
@@ -747,7 +746,7 @@ let pushIPatNoop = function
| pats :: orpat -> (IPatNoop :: pats) :: orpat
| [] -> []
-let test_ident_no_do strm =
+let test_ident_no_do _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT s when s <> "do" -> ()
| _ -> raise Stream.Failure
@@ -825,7 +824,7 @@ END
{
-let reject_ssrhid strm =
+let reject_ssrhid _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "[" ->
(match Util.stream_nth 1 strm with
@@ -835,13 +834,13 @@ let reject_ssrhid strm =
let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
-let rec reject_binder crossed_paren k s =
+let rec reject_binder crossed_paren k tok s =
match
try Some (Util.stream_nth k s)
with Stream.Failure -> None
with
- | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s
- | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s
+ | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s
+ | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s
| Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
raise Stream.Failure
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
@@ -1006,7 +1005,7 @@ END
{
-let accept_ssrfwdid strm =
+let accept_ssrfwdid _ strm =
match stream_nth 0 strm with
| Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
| _ -> raise Stream.Failure
@@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
| [ ssrbvar(bv) ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ")" ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
{ let x = bvar_lname bv in
(FwdPose, [BFdecl 1]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
{ let xs = List.map bvar_lname (bv :: bvs) in
let n = List.length xs in
(FwdPose, [BFdecl n]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
{ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram
ssrbinder: [
[ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ]
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
END
@@ -1391,7 +1390,7 @@ let push_binders c2 bs =
let rec fix_binders = let open CAst in function
| (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
- CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
+ CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
| (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
CLocalDef (x, v, oty) :: fix_binders bs
| _ -> []
@@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function
| IPatId id ->
let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
- CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
+ CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
mkCHole None)
| _ -> anomaly "non-id accepted as binder")
@@ -1590,7 +1589,7 @@ END
let sq_brace_tacnames =
["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
(* "by" is a keyword *)
-let accept_ssrseqvar strm =
+let accept_ssrseqvar _ strm =
match stream_nth 0 strm with
| Tok.IDENT id when not (List.mem id sq_brace_tacnames) ->
accept_before_syms_or_ids ["["] ["first";"last"] strm
@@ -1684,7 +1683,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 = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
}
@@ -1987,7 +1986,7 @@ END
{
-let accept_ssreqid strm =
+let accept_ssreqid _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT _ -> accept_before_syms [":"] strm
| Tok.KEYWORD ":" -> ()
@@ -2406,7 +2405,7 @@ let lbrace = Char.chr 123
(** Workaround to a limitation of coqpp *)
let test_ssr_rw_syntax =
- let test strm =
+ let test _ strm =
if not !ssr_rw_syntax then raise Stream.Failure else
if is_ssr_loaded () then () else
match Util.stream_nth 0 strm with
@@ -2617,7 +2616,7 @@ END
{
-let accept_idcomma strm =
+let accept_idcomma _ strm =
match stream_nth 0 strm with
| Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
| _ -> raise Stream.Failure
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0adabb0673..f3f1d713e9 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -27,7 +27,6 @@ open Notation_ops
open Notation_term
open Glob_term
open Stdarg
-open Decl_kinds
open Pp
open Ppconstr
open Printer
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:36:51 +0000