aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh2
-rw-r--r--doc/changelog/02-specification-language/13911-master.rst4
-rw-r--r--doc/sphinx/addendum/program.rst11
-rw-r--r--doc/sphinx/language/core/definitions.rst4
-rw-r--r--doc/tools/docgram/common.edit_mlg1
-rw-r--r--doc/tools/docgram/fullGrammar19
-rw-r--r--doc/tools/docgram/orderedGrammar1
-rw-r--r--interp/constrexpr_ops.ml5
-rw-r--r--interp/notation_ops.ml8
-rw-r--r--parsing/g_constr.mlg4
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--pretyping/glob_ops.ml9
-rw-r--r--pretyping/glob_term.ml1
-rw-r--r--pretyping/pretyping.ml3
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--printing/proof_diffs.ml1
-rw-r--r--theories/Classes/EquivDec.v2
-rw-r--r--theories/Classes/SetoidDec.v2
-rw-r--r--theories/Program/Utils.v2
19 files changed, 26 insertions, 58 deletions
diff --git a/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh
new file mode 100644
index 0000000000..29f2386797
--- /dev/null
+++ b/dev/ci/user-overlays/13911-Zimmi48-remove_type_cast.sh
@@ -0,0 +1,2 @@
+overlay equations https://github.com/Zimmi48/Coq-Equations coq-13911 13911 remove_type_cast
+overlay elpi https://github.com/Zimmi48/coq-elpi patch-1 13911 remove_type_cast
diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst
new file mode 100644
index 0000000000..a0b37dd2d9
--- /dev/null
+++ b/doc/changelog/02-specification-language/13911-master.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ The little used `:>` type cast, which was only interpreted in Program-mode
+ (`#13911 <https://github.com/coq/coq/pull/13911>`_,
+ by Jim Fehrle and Théo Zimmermann).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a011c81f15..52e47b52ae 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in:
The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
produce an equality, contrary to the let pattern construct
:g:`let '(x1,..., xn) := t in b`.
-Also, :g:`term :>` explicitly asks the system to
-coerce term to its support type. It can be useful in notations, for
-example:
-
-.. coqtop:: all
-
- Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
-
-This notation denotes equality on subset types using equality on their
-support types, avoiding uses of proof-irrelevance that would come up
-when reasoning with equality on the subset types themselves.
The next two commands are similar to their standard counterparts
:cmd:`Definition` and :cmd:`Fixpoint`
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index fcf61a5bf4..1a729ced4e 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -42,7 +42,6 @@ Type cast
term_cast ::= @term10 : @type
| @term10 <: @type
| @term10 <<: @type
- | @term10 :>
The expression :n:`@term10 : @type` is a type cast expression. It enforces
the type of :n:`@term10` to be :n:`@type`.
@@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`).
:n:`@term10 <<: @type` specifies that compilation to OCaml will be used
to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`).
-:n:`@term10 :>` casts to the support type in Program mode.
-See :ref:`syntactic_control`.
-
.. _gallina-definitions:
Top-level definitions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fd1c3c0260..5c211d82e9 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
| REPLACE term99 ":" term200
| WITH term99 ":" type
| MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
]
constr: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ab1a9d4c75..1f5c1ee3e2 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,6 +1,15 @@
(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)
DOC_GRAMMAR
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
Constr.ident: [
| Prim.ident
]
@@ -75,7 +84,6 @@ term100: [
| term99 "<:" term200
| term99 "<<:" term200
| term99 ":" term200
-| term99 ":>"
| term99
]
@@ -478,15 +486,6 @@ strategy_level: [
| "transparent"
]
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
opt_hintbases: [
|
| ":" LIST1 IDENT
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 5b19b7fc55..49bcf97850 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -553,7 +553,6 @@ term_cast: [
| term10 ":" type
| term10 "<:" type
| term10 "<<:" type
-| term10 ":>"
]
term_match: [
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f02874253e..40fe13784a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with
| CastConv t1, CastConv t2
| CastVM t1, CastVM t2
| CastNative t1, CastNative t2 -> constr_expr_eq t1 t2
-| CastCoerce, CastCoerce -> true
| CastConv _, _
| CastVM _, _
-| CastNative _, _
-| CastCoerce, _ -> false
+| CastNative _, _ -> false
let constr_loc c = CAst.(c.loc)
let cases_pattern_expr_loc cp = CAst.(cp.loc)
@@ -343,7 +341,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
| CLetIn (na,a,t,b) ->
f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
| CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
- | CCast (a,CastCoerce) -> f n acc a
| CNotation (_,_,(l,ll,bl,bll)) ->
(* The following is an approximation: we don't know exactly if
an ident is binding nor to which subterms bindings apply *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ea5e2a1ad4..ea95655c18 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function
let cast_type_iter2 f t1 t2 = match t1, t2 with
| CastConv t1, CastConv t2 -> f t1 t2
| CastVM t1, CastVM t2 -> f t1 t2
- | CastCoerce, CastCoerce -> ()
| CastNative t1, CastNative t2 -> f t1 t2
- | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit
+ | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit
(* used to update the notation variable with the local variables used
in NList and NBinderList, since the iterator has its own variable *)
@@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 =
| CastVM t1, CastVM t2
| CastNative t1, CastNative t2 ->
match_fun sigma t1 t2
- | CastCoerce, CastCoerce ->
- sigma
| CastConv _, _
| CastVM _, _
- | CastNative _, _
- | CastCoerce, _ -> raise No_match
+ | CastNative _, _ -> raise No_match
let does_not_come_from_already_eta_expanded_var glob =
(* This is hack to avoid looping on a rule with rhs of the form *)
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index efe4bfd7f6..d0d1071c26 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -151,9 +151,7 @@ GRAMMAR EXTEND Gram
| c1 = term; "<<:"; c2 = term LEVEL "200" ->
{ CAst.make ~loc @@ CCast(c1, CastNative c2) }
| c1 = term; ":"; c2 = term LEVEL "200" ->
- { CAst.make ~loc @@ CCast(c1, CastConv c2) }
- | c1 = term; ":>" ->
- { CAst.make ~loc @@ CCast(c1, CastCoerce) } ]
+ { CAst.make ~loc @@ CCast(c1, CastConv c2) } ]
| "99" RIGHTA [ ]
| "90" RIGHTA [ ]
| "10" LEFTA
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 164a446fe3..fb00d2f202 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -342,7 +342,7 @@ let is_free_in id =
| GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ -> false
| GHole _ -> false
| GCast (b, (CastConv t | CastVM t | CastNative t)) ->
- is_free_in b || is_free_in t | GCast (b, CastCoerce) -> is_free_in b
+ is_free_in b || is_free_in t
| GInt _ | GFloat _ -> false
| GArray (_u, t, def, ty) ->
Array.exists is_free_in t || is_free_in def || is_free_in ty)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 86d2cc78e0..5a8ac32ffa 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -104,9 +104,8 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
let cast_type_eq eq t1 t2 = match t1, t2 with
| CastConv t1, CastConv t2 -> eq t1 t2
| CastVM t1, CastVM t2 -> eq t1 t2
- | CastCoerce, CastCoerce -> true
| CastNative t1, CastNative t2 -> eq t1 t2
- | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false
+ | (CastConv _ | CastVM _ | CastNative _), _ -> false
let matching_var_kind_eq k1 k2 = match k1, k2 with
| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
@@ -188,14 +187,12 @@ let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
let map_cast_type f = function
| CastConv a -> CastConv (f a)
| CastVM a -> CastVM (f a)
- | CastCoerce -> CastCoerce
| CastNative a -> CastNative (f a)
let smartmap_cast_type f c =
match c with
| CastConv a -> let a' = f a in if a' == a then c else CastConv a'
| CastVM a -> let a' = f a in if a' == a then c else CastVM a'
- | CastCoerce -> CastCoerce
| CastNative a -> let a' = f a in if a' == a then c else CastNative a'
let map_glob_constr_left_to_right f = DAst.map (function
@@ -275,7 +272,7 @@ let fold_glob_constr f acc = DAst.with_val (function
Array.fold_left f (Array.fold_left f acc tyl) bv
| GCast (c,k) ->
let acc = match k with
- | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
+ | CastConv t | CastVM t | CastNative t -> f acc t in
f acc c
| GArray (_u,t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc
@@ -318,7 +315,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
Array.fold_left_i f' acc idl
| GCast (c,k) ->
let acc = match k with
- | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
+ | CastConv t | CastVM t | CastNative t -> f v acc t in
f v acc c
| GArray (_u, t, def, ty) -> f v (f v (Array.fold_left (f v) acc t) def) ty
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc))
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 9f93e5e6c1..d480c12834 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -57,7 +57,6 @@ and glob_fix_kind =
type 'a cast_type =
| CastConv of 'a
| CastVM of 'a
- | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
| CastNative of 'a
(** The kind of patterns that occurs in "match ... with ... end"
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index de1af62043..cb52e32cd5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1165,9 +1165,6 @@ struct
let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in
let sigma, cj =
match k with
- | CastCoerce ->
- let sigma, cj = pretype empty_tycon env sigma c in
- Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj
| CastConv t | CastVM t | CastNative t ->
let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 4c410c3170..e08a494c2e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -673,8 +673,7 @@ let tag_var = tag Tag.variable
match b with
| CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
| CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
- | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
- | CastCoerce -> str ":>"),
+ | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b),
lcast
)
| CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 9bf765717f..9ba64717d9 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -529,7 +529,6 @@ let match_goals ot nt =
| CastVM a, CastVM a2
| CastNative a, CastNative a2 ->
constr_expr ogname a a2
- | CastCoerce, CastCoerce -> ()
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
| CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
constr_notation_substitution ogname args args2
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index a1a4da6f37..575d773c77 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -43,7 +43,7 @@ Class EqDec A R {equiv : Equivalence R} :=
take precedence of [==] defined in the type scope, hence we can have both
at the same time. *)
-Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
+Notation " x == y " := (equiv_dec x y) (no associativity, at level 70) : equiv_scope.
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
match x with
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index f4220e3aa1..435dacbd4c 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -42,7 +42,7 @@ Class EqDec `(S : Setoid A) :=
take precedence of [==] defined in the type scope, hence we can have both
at the same time. *)
-Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+Notation " x == y " := (equiv_dec x y) (no associativity, at level 70).
Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
match x with
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index b2bdd8099a..717e3191ea 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -33,8 +33,6 @@ Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scop
(** Coerces objects to their support before comparing them. *)
-Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope.
-
Require Import Coq.Bool.Sumbool.
(** Construct a dependent disjunction from a boolean. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:00:55 +0000