Merge PR coq#18031: [ssr] Rm cast notation

Reviewed-by: herbelin Ack-by: gares Co-authored-by: herbelin <[email protected]>
SkySkimmer · Sep 29, 2023 · a2bf792 · a2bf792
2 parents 4f1fda3 + 6703fb9
commit a2bf792
Showing 1 changed file with 0 additions and 10 deletions.
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
@@ -111,8 +111,6 @@ Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200,
 Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200,
   c, R, vT, vF at level 200, x name).
 
-Reserved Notation "x : T" (at level 100, right associativity,
-  format "'[hv' x '/ '  :  T ']'").
 Reserved Notation "T : 'Type'" (at level 100, format "T  :  'Type'").
 Reserved Notation "P : 'Prop'" (at level 100, format "P  :  'Prop'").
 
@@ -184,14 +182,6 @@ Declare Scope form_scope.
 Delimit Scope form_scope with FORM.
 Open Scope form_scope.
 
-(**
- Allow overloading of the cast (x : T) syntax, put whitespace around the
- ":" symbol to avoid lexical clashes (and for consistency with the parsing
- precedence of the notation, which binds less tightly than application),
- and put printing boxes that print the type of a long definition on a
- separate line rather than force-fit it at the right margin.                 **)
-Notation "x : T" := (CoqCast x T) : core_scope.
-
 (**
  Allow the casual use of notations like nat * nat for explicit Type
  declarations. Note that (nat * nat : Type) is NOT equivalent to