aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/ground.ml16
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/ltac/tacentries.ml11
-rw-r--r--plugins/ltac/tacenv.mli2
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml414
-rw-r--r--plugins/ssrmatching/ssrmatching.ml8
7 files changed, 21 insertions, 34 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 4e3ba57308..516b04ea21 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -13,23 +13,21 @@ open Formula
open Sequent
open Rules
open Instances
-open Constr
open Tacmach.New
open Tacticals.New
+open Globnames
let update_flags ()=
- let predref=ref Names.Cpred.empty in
- let f coe=
- try
- let kn= fst (destConst (Classops.get_coercion_value coe)) in
- predref:=Names.Cpred.add kn !predref
- with DestKO -> ()
+ let f acc coe =
+ match coe.Classops.coe_value with
+ | ConstRef c -> Names.Cpred.add c acc
+ | _ -> acc
in
- List.iter f (Classops.coercions ());
+ let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
- (Names.Id.Pred.full,Names.Cpred.complement !predref)
+ (Names.Id.Pred.full,Names.Cpred.complement pred)
let ground_tac solver startseq =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 439274240f..ad11f853ca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -351,7 +351,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
Locusops.onConcl);
observe_tac ("toto ") tclIDTAC;
- (* introducing the the result of the graph and the equality hypothesis *)
+ (* introducing the result of the graph and the equality hypothesis *)
observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
(* replacing [res] with its value *)
observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4b834d66d3..636cb8ebf8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -594,15 +594,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol
let clause_of_ty_ml = function
| TyML (t,_) -> clause_of_sign t
-let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
- | TUentry a -> ExtraArg a
- | TUentryl (a,l) -> ExtraArg a
- | TUopt(o) -> OptArg (prj o)
- | TUlist1 l -> ListArg (prj l)
- | TUlist1sep (l,_) -> ListArg (prj l)
- | TUlist0 l -> ListArg (prj l)
- | TUlist0sep (l,_) -> ListArg (prj l)
-
let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
fun sign tac ->
match sign with
@@ -617,7 +608,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i
begin fun tac vals ist -> match vals with
| [] -> assert false
| v :: vals ->
- let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in
f (tac v') vals ist
end tac
| TyAnonArg (a, sig') -> eval_sign sig' tac
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 7143f51853..d5d36c97fa 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -41,7 +41,7 @@ val register_alias : alias -> alias_tactic -> unit
(** Register a tactic alias. *)
val interp_alias : alias -> alias_tactic
-(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+(** Recover the body of an alias. Raises an anomaly if it does not exist. *)
val check_alias : alias -> bool
(** Returns [true] if an alias is defined, false otherwise. *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 54f3f9c718..1f3c758e5c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
(* term mkApp (t', args) is convertible to t. *)
(* This makes a useful shorthand for local definitions in proofs, *)
(* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *)
-(* and, in context of the the 4CT library, pose mid := maps id means *)
+(* and, in context of the 4CT library, pose mid := maps id means *)
(* pose mid := fun d : detaSet => @maps d d (@id (datum d)) *)
(* Note that this facility does not extend to set, which tries *)
(* instead to fill holes by matching a goal subterm. *)
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7ce2dd64af..989a6c5bf1 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -24,7 +24,6 @@ open Ltac_plugin
open Notation_ops
open Notation_term
open Glob_term
-open Globnames
open Stdarg
open Genarg
open Decl_kinds
@@ -218,8 +217,8 @@ let interp_search_notation ?loc tag okey =
(Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
loop 0 1 in
- let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in
- let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in
+ let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+ let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
let pr_and_list pr = function
| [x] -> pr x
| x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
@@ -294,7 +293,7 @@ let interp_search_notation ?loc tag okey =
let scs' = List.remove (=) sc !scs in
let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
Feedback.msg_warning (hov 4 w)
- else if String.string_contains ~where:ntn ~what:" .. " then
+ else if String.string_contains ~where:(snd ntn) ~what:" .. " then
err (pr_ntn ntn ++ str " is an n-ary notation");
let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
let rec sub () = function
@@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat =
true, cp
with _ -> false, [] in
let coerce hp coe_index =
- let coe = Classops.get_coercion_value coe_index in
+ let coe_ref = coe_index.Classops.coe_value in
try
- let coe_ref = global_of_constr coe in
let n_imps = Option.get (Classops.hide_coercion coe_ref) in
mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
- with _ ->
- errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
+ with Not_found | Option.IsNone ->
+ errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
++ str "to interpret head search pattern as type") in
filter_head, List.fold_left coerce hpat' coe_path
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 05eda14e90..30a998c6ce 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -929,7 +929,7 @@ let glob_cpattern gs p =
| k, (v, Some t), _ as orig ->
if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
match t.CAst.v with
- | CNotation("( _ in _ )", ([t1; t2], [], [], [])) ->
+ | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
(try match glob t1, glob t2 with
| (r1, None), (r2, None) -> encode k "In" [r1;r2]
| (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -937,11 +937,11 @@ let glob_cpattern gs p =
| (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
| _ -> CErrors.anomaly (str"where are we?.")
with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
- | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) ->
+ | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
- | CNotation("( _ as _ )", ([t1; t2], [], [], [])) ->
+ | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
encode k "As" [fst (glob t1); fst (glob t2)]
- | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) ->
+ | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
| _ -> glob_ssrterm gs orig
;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:11:13 +0000