aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml2
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/extraction/ExtrHaskellString.v2
-rw-r--r--plugins/extraction/ExtrOcamlString.v1
-rw-r--r--plugins/extraction/extraction.ml24
-rw-r--r--plugins/firstorder/ground.ml16
-rw-r--r--plugins/ltac/tacentries.ml11
-rw-r--r--plugins/ssr/ssrbool.v16
-rw-r--r--plugins/ssr/ssreflect.v6
-rw-r--r--plugins/ssr/ssrfun.v4
-rw-r--r--plugins/ssr/ssrvernac.ml414
-rw-r--r--plugins/ssrmatching/ssrmatching.ml8
12 files changed, 49 insertions, 59 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4a691e442c..ce620d5312 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -460,7 +460,7 @@ let rec canonize_name sigma c =
mkApp (func ct,Array.Smart.map func l)
| Proj(p,c) ->
let p' = Projection.map (fun kn ->
- Constant.make1 (Constant.canonical kn)) p in
+ MutInd.make1 (MutInd.canonical kn)) p in
(mkProj (p', func c))
| _ -> c
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 04ff11fc49..2eaa6146e1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -84,8 +84,8 @@ let rec decompose_term env sigma t=
let canon_const = Constant.make1 (Constant.canonical c) in
(Symb (Constr.mkConstU (canon_const,u)))
| Proj (p, c) ->
- let canon_const kn = Constant.make1 (Constant.canonical kn) in
- let p' = Projection.map canon_const p in
+ let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in
+ let p' = Projection.map canon_mind p in
let c = Retyping.expand_projection env sigma p' c [] in
decompose_term env sigma c
| _ ->
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index ac1f6f9130..a4a40d3c5a 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -35,6 +35,8 @@ Extract Inductive ascii => "Prelude.Char"
(Data.Bits.testBit (Data.Char.ord a) 6)
(Data.Bits.testBit (Data.Char.ord a) 7))".
Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
Extract Inlined Constant String.string_dec => "(Prelude.==)".
+Extract Inlined Constant String.eqb => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 030b486b26..a2a6a8fe67 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -33,6 +33,7 @@ Extract Constant shift =>
"fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
Extract Inlined Constant ascii_dec => "(=)".
+Extract Inlined Constant Ascii.eqb => "(=)".
Extract Inductive string => "char list" [ "[]" "(::)" ].
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 71e09992cc..67c605ea1d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,13 +1065,13 @@ let extract_constant env kn cb =
(match cb.const_body with
| Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
- (match Environ.is_projection kn env with
- | false -> mk_typ (get_body c)
- | true ->
- let pb = lookup_projection (Projection.make kn false) env in
- let ind = pb.Declarations.proj_ind in
+ (match Recordops.find_primitive_projection kn with
+ | None -> mk_typ (get_body c)
+ | Some p ->
+ let p = Projection.make p false in
+ let ind = Projection.inductive p in
let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(pb.Declarations.proj_arg) in
+ let body = bodies.(Projection.arg p) in
mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
@@ -1081,13 +1081,13 @@ let extract_constant env kn cb =
(match cb.const_body with
| Undef _ -> warn_info (); mk_ax ()
| Def c ->
- (match Environ.is_projection kn env with
- | false -> mk_def (get_body c)
- | true ->
- let pb = lookup_projection (Projection.make kn false) env in
- let ind = pb.Declarations.proj_ind in
+ (match Recordops.find_primitive_projection kn with
+ | None -> mk_def (get_body c)
+ | Some p ->
+ let p = Projection.make p false in
+ let ind = Projection.inductive p in
let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(pb.Declarations.proj_arg) in
+ let body = bodies.(Projection.arg p) in
mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
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/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/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 7d05b64384..0865f75ec5 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -61,8 +61,8 @@ Require Import ssreflect ssrfun.
(* classically P <-> we can assume P when proving is_true b. *)
(* := forall b : bool, (P -> b) -> b. *)
(* This is equivalent to ~ (~ P) when P : Prop. *)
-(* implies P Q == wrapper coinductive type that coerces to P -> Q *)
-(* and can be used as a P -> Q view unambigously. *)
+(* implies P Q == wrapper variant type that coerces to P -> Q and *)
+(* can be used as a P -> Q view unambigously. *)
(* Useful to avoid spurious insertion of <-> views *)
(* when Q is a conjunction of foralls, as in Lemma *)
(* all_and2 below; conversely, avoids confusion in *)
@@ -456,7 +456,7 @@ Section BoolIf.
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
-CoInductive if_spec (not_b : Prop) : bool -> A -> Set :=
+Variant if_spec (not_b : Prop) : bool -> A -> Set :=
| IfSpecTrue of b : if_spec not_b true vT
| IfSpecFalse of not_b : if_spec not_b false vF.
@@ -585,7 +585,7 @@ Lemma rwP2 : reflect Q b -> (P <-> Q).
Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed.
(* Predicate family to reflect excluded middle in bool. *)
-CoInductive alt_spec : bool -> Type :=
+Variant alt_spec : bool -> Type :=
| AltTrue of P : alt_spec true
| AltFalse of ~~ b : alt_spec false.
@@ -603,7 +603,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
(* Allow the direct application of a reflection lemma to a boolean assertion. *)
Coercion elimT : reflect >-> Funclass.
-CoInductive implies P Q := Implies of P -> Q.
+Variant implies P Q := Implies of P -> Q.
Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed.
Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
Proof. by case=> iP ? /iP. Qed.
@@ -1119,7 +1119,7 @@ Proof. by move=> *; apply/orP; left. Qed.
Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
Proof. by move=> *; apply/orP; right. Qed.
-CoInductive mem_pred := Mem of pred T.
+Variant mem_pred := Mem of pred T.
Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).
@@ -1329,7 +1329,7 @@ End simpl_mem.
(* Qualifiers and keyed predicates. *)
-CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
+Variant qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x => let: Qualifier _ p := q in p x.
@@ -1376,7 +1376,7 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
Section KeyPred.
Variable T : Type.
-CoInductive pred_key (p : predPredType T) := DefaultPredKey.
+Variant pred_key (p : predPredType T) := DefaultPredKey.
Variable p : predPredType T.
Structure keyed_pred (k : pred_key p) :=
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b0a9441385..b4144aa45e 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -184,7 +184,7 @@ Inductive external_view : Type := tactic_view of Type.
Module TheCanonical.
-CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put.
+Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
@@ -275,10 +275,10 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
(* We also define a simpler version ("phant" / "Phant") of phantom for the *)
(* common case where p_type is Type. *)
-CoInductive phantom T (p : T) := Phantom.
+Variant phantom T (p : T) := Phantom.
Arguments phantom : clear implicits.
Arguments Phantom : clear implicits.
-CoInductive phant (p : Type) := Phant.
+Variant phant (p : Type) := Phant.
(* Internal tagging used by the implementation of the ssreflect elim. *)
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index ac2c78249b..b2d5143e36 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -326,7 +326,7 @@ Section SimplFun.
Variables aT rT : Type.
-CoInductive simpl_fun := SimplFun of aT -> rT.
+Variant simpl_fun := SimplFun of aT -> rT.
Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
@@ -684,7 +684,7 @@ Section Bijections.
Variables (A B : Type) (f : B -> A).
-CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.
+Variant bijective : Prop := Bijective g of cancel f g & cancel g f.
Hypothesis bijf : bijective.
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-05-03 01:13:56 +0000