Merge PR #13911: Remove the :> type cast?

Reviewed-by: mattam82
Ack-by: Zimmi48

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 0c8980b1bd..fe166524bf 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 40bb980e90..2b09263cc4 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 21b2137f09..4c2fc26b45 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1166,9 +1166,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. *)