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/ssr/ssrbool.v16
-rw-r--r--plugins/ssr/ssreflect.v6
-rw-r--r--plugins/ssr/ssrfun.v4
8 files changed, 31 insertions, 28 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/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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:21:22 +0000