Print REVERTcast as "c :> t" in Printing All mode, and parse it.

doc/sphinx/language/core/definitions.rst

@@ -40,6 +40,7 @@ Type cast
 
 .. prodn::
    term_cast ::= @term10 : @type
+   | @term10 :> @type
    | @term10 <: @type
    | @term10 <<: @type
 

doc/tools/docgram/common.edit_mlg

@@ -373,6 +373,9 @@ term100: [
 | REPLACE term99 ":" term200
 | WITH term99 ":" type
 | MOVETO term_cast term99 ":" type
+| REPLACE term99 ":>" term200
+| WITH term99 ":>" type
+| MOVETO term_cast term99 ":>" type
 ]
 
 constr: [

doc/tools/docgram/fullGrammar

@@ -74,6 +74,7 @@ term200: [
 term100: [
 | term99 "<:" term200
 | term99 "<<:" term200
+| term99 ":>" term200
 | term99 ":" term200
 | term99
 ]

doc/tools/docgram/orderedGrammar

@@ -551,6 +551,7 @@ term_generalizing: [
 
 term_cast: [
 | term10 ":" type
+| term10 ":>" type
 | term10 "<:" type
 | term10 "<<:" type
 ]

interp/constrexpr.ml

@@ -128,7 +128,7 @@ and constr_expr_r =
   | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name CAst.t * (lident * constr_expr) list
   | CSort   of sort_expr
-  | CCast   of constr_expr * Glob_term.cast_type * constr_expr
+  | CCast   of constr_expr * Constr.cast_kind * constr_expr
   | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
   | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token

interp/constrexpr_ops.ml

@@ -242,7 +242,7 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end)
       | CSort s1, CSort s2 ->
         sort_expr_eq s1 s2
       | CCast(c1,k1,t1), CCast(c2,k2,t2) ->
-        constr_expr_eq c1 c2 && Glob_ops.cast_type_eq k1 k2 && constr_expr_eq t1 t2
+        constr_expr_eq c1 c2 && Glob_ops.cast_kind_eq k1 k2 && constr_expr_eq t1 t2
       | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
         Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
         notation_eq n1 n2 &&
@@ -674,7 +674,7 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
   | CDelimiters (s,p) ->
      CPatDelimiters (s,coerce_to_cases_pattern_expr p)
-  | CCast (p,CastConv, t) ->
+  | CCast (p,Constr.DEFAULTcast, t) ->
      CPatCast (coerce_to_cases_pattern_expr p,t)
   | _ ->
      CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"

interp/constrexpr_ops.mli

@@ -49,7 +49,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
 
 val mkIdentC : Id.t -> constr_expr
 val mkRefC : qualid -> constr_expr
-val mkCastC : constr_expr * Glob_term.cast_type * constr_expr -> constr_expr
+val mkCastC : constr_expr * Constr.cast_kind * constr_expr -> constr_expr
 val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
 val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr

interp/notation_ops.ml

@@ -201,7 +201,7 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
   | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> ()
   | NCast (c1, k1, t1), NCast (c2, k2, t2) ->
     aux vars renaming c1 c2;
-    if not (cast_type_eq k1 k2) then raise Exit;
+    if not (cast_kind_eq k1 k2) then raise Exit;
     aux vars renaming t1 t2
   | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
   | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
@@ -1436,7 +1436,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
   | GCast(c1, k1, t1), NCast(c2, k2, t2) ->
     let sigma = match_in u alp metas sigma c1 c2 in
-    if not (cast_type_eq k1 k2) then raise No_match;
+    if not (cast_kind_eq k1 k2) then raise No_match;
     match_in u alp metas sigma t1 t2
 
   (* Next pair of lines useful only if not coming from detyping *)

interp/notation_term.ml

@@ -43,7 +43,7 @@ type notation_constr =
       (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort
-  | NCast of notation_constr * cast_type * notation_constr
+  | NCast of notation_constr * Constr.cast_kind * notation_constr
   | NInt of Uint63.t
   | NFloat of Float64.t
   | NArray of notation_constr array * notation_constr * notation_constr

parsing/g_constr.mlg

@@ -30,7 +30,7 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
     let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
-    in CAst.make ?loc @@ CCast(c, CastConv, ty)
+    in CAst.make ?loc @@ CCast(c, DEFAULTcast, ty)
 
 let binder_of_name expl { CAst.loc = loc; v = na } =
   CLocalAssum ([CAst.make ?loc na], Default expl,
@@ -147,11 +147,13 @@ GRAMMAR EXTEND Gram
       [ c = binder_constr -> { c } ]
     | "100" RIGHTA
       [ c1 = term; "<:"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastVM, c2) }
+                 { CAst.make ~loc @@ CCast(c1, VMcast, c2) }
       | c1 = term; "<<:"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastNative, c2) }
+                 { CAst.make ~loc @@ CCast(c1, NATIVEcast, c2) }
+      | c1 = term; ":>"; c2 = term LEVEL "200" ->
+                 { CAst.make ~loc @@ CCast(c1, REVERTcast, c2) }
       | c1 = term; ":"; c2 = term LEVEL "200" ->
-                 { CAst.make ~loc @@ CCast(c1, CastConv, c2) } ]
+                 { CAst.make ~loc @@ CCast(c1, DEFAULTcast, c2) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
@@ -222,7 +224,7 @@ GRAMMAR EXTEND Gram
       | "let"; id=name; bl = binders; ty = let_type_cstr; ":=";
         c1 = term LEVEL "200"; "in"; c2 = term LEVEL "200" ->
         { let ty,c1 = match ty, c1 with
-          | (_,None), { CAst.v = CCast(c, CastConv, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+          | (_,None), { CAst.v = CCast(c, DEFAULTcast, t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
           CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1,
                  Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) }
@@ -418,7 +420,7 @@ GRAMMAR EXTEND Gram
         { [CLocalAssum ([id],Default Explicit,c)] }
       | "("; id = name; ":="; c = lconstr; ")" ->
         { match c.CAst.v with
-          | CCast(c, CastConv, t) -> [CLocalDef (id,c,Some t)]
+          | CCast(c, DEFAULTcast, t) -> [CLocalDef (id,c,Some t)]
           | _ -> [CLocalDef (id,c,None)] }
       | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
         { [CLocalDef (id,c,Some t)] }

plugins/funind/glob_term_to_relation.ml

@@ -626,7 +626,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
     let v =
       match typ with
       | None -> v
-      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv, t)
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, DEFAULTcast, t)
     in
     let v_res = build_entry_lc env sigma funnames avoid v in
     let v_as_constr, ctx = Pretyping.understand env (Evd.from_env env) v in
@@ -1130,7 +1130,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     let t =
       match t with
       | None -> v
-      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, CastConv, t)
+      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, DEFAULTcast, t)
     in
     let not_free_in_t id = not (is_free_in id t) in
     let evd = Evd.from_env env in

plugins/ssr/ssrcommon.ml

@@ -194,7 +194,7 @@ let rec isRHoles cl = match cl with
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
 let mkRVar id = DAst.make @@ GRef (GlobRef.VarRef id,None)
 let mkRltacVar id = DAst.make @@ GVar (id)
-let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv, rt)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, DEFAULTcast, rt)
 let mkRType =  DAst.make @@ GSort (UAnonymous {rigid=true})
 let mkRProp =  DAst.make @@ GSort (UNamed [GProp,0])
 let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
@@ -905,7 +905,7 @@ let mkCLambda ?loc name ty t =  CAst.make ?loc @@
    CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
    CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t)
-let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv, ty)
+let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, DEFAULTcast, ty)
 
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
 let rec isCxHoles = function ({ CAst.v = CHole _ }, None) :: ch -> isCxHoles ch | _ -> false

plugins/ssr/ssrfwd.ml

@@ -157,13 +157,13 @@ let havetac ist
     let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in
   let open CAst in
   let ct, cty, hole, loc = match Ssrcommon.ssrterm_of_ast_closure_term t with
-    | _, (_, Some { loc; v = CCast (ct, CastConv, cty)}) ->
+    | _, (_, Some { loc; v = CCast (ct, DEFAULTcast, cty)}) ->
       mkt ct, mkt cty, mkt (mkCHole None), loc
     | _, (_, Some ct) ->
       mkt ct, mkt (mkCHole None), mkt (mkCHole None), None
     | _, (t, None) ->
       begin match DAst.get t with
-      | GCast (ct, CastConv, cty) ->
+      | GCast (ct, DEFAULTcast, cty) ->
         mkl ct, mkl cty, mkl mkRHole, t.CAst.loc
       | _ -> mkl t, mkl mkRHole, mkl mkRHole, None
       end
@@ -238,12 +238,12 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave =
   let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with
   | (a, (b, Some ct)) ->
     begin match ct.CAst.v with
-    | CCast (_, CastConv, cty) -> a, (b, Some cty)
+    | CCast (_, DEFAULTcast, cty) -> a, (b, Some cty)
     | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
     end
   | (a, (t, None)) ->
     begin match DAst.get t with
-    | GCast (_, CastConv, cty) -> a, (cty, None)
+    | GCast (_, DEFAULTcast, cty) -> a, (cty, None)
     | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
     end
   in
@@ -325,12 +325,12 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let c = match Ssrcommon.ssrterm_of_ast_closure_term c with
   | (a, (b, Some ct)) ->
     begin match ct.CAst.v with
-    | CCast (_, CastConv, cty) -> a, (b, Some cty)
+    | CCast (_, DEFAULTcast, cty) -> a, (b, Some cty)
     | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
     end
   | (a, (t, None)) ->
     begin match DAst.get t with
-    | GCast (_, CastConv, cty) -> a, (cty, None)
+    | GCast (_, DEFAULTcast, cty) -> a, (cty, None)
     | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
     end
   in

plugins/ssr/ssrparser.mlg

@@ -12,7 +12,8 @@
 
 {
 
-let _vmcast = Constr.VMcast
+let defaultCast = Constr.DEFAULTcast
+let vmCast = Constr.VMcast
 open Names
 open Pp
 open Pcoq
@@ -1229,7 +1230,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = CCast (c, Glob_term.CastConv, t) } ->
+  | [BFcast], { v = CCast (c, defaultCast, t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h,
     { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
@@ -1271,7 +1272,7 @@ let mkFwdCast fk ?loc ?c t =
     | Some c -> assert (same_ist t c); c.body in
   ((fk, [BFcast]),
    { t with annotation = `None;
-            body = (CAst.make ?loc @@ CCast (c, Glob_term.CastConv, t.body)) })
+            body = (CAst.make ?loc @@ CCast (c, defaultCast, t.body)) })
 
 let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t))
 
@@ -1386,8 +1387,8 @@ let push_binders c2 bs =
   | [] -> c
   | _ -> anomaly "binder not a lambda nor a let in" in
   match c2 with
-  | { loc; v = CCast (ct, Glob_term.CastConv, cty) } ->
-      CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv, (loop true cty bs)))
+  | { loc; v = CCast (ct, defaultCast, cty) } ->
+      CAst.make ?loc @@ (CCast (loop false ct bs, defaultCast, (loop true cty bs)))
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
@@ -2213,7 +2214,7 @@ END
 
 let vmexacttac pf =
   Goal.enter begin fun gl ->
-  exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
+  exact_no_check (EConstr.mkCast (pf, vmCast, Tacmach.New.pf_concl gl))
   end
 
 }

plugins/ssrmatching/ssrmatching.ml

@@ -135,12 +135,12 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@
    CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((CAst.make ?loc name), bo, None, t)
-let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv, ty)
+let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, DEFAULTcast, ty)
 
 (** Constructors for rawconstr *)
 let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
-let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv, rt)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, DEFAULTcast, rt)
 let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 let nf_evar sigma c =
@@ -988,7 +988,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   let ist_of x = x.interpretation in
   let decode ({interpretation=ist; _} as t) ?reccall f g =
     try match DAst.get (pf_intern_term env sigma0 t) with
-    | GCast(t, CastConv, c) when isGHole t && isGLambda c->
+    | GCast(t, DEFAULTcast, c) when isGHole t && isGLambda c->
       let (x, c) = destGLambda c in
       f x {kind = NoFlag; pattern = (c,None); interpretation = ist}
     | GVar id
@@ -1035,7 +1035,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   let red = let rec decode_red = function
     | T {kind=k; pattern=(t,None); interpretation=ist} ->
       begin match DAst.get t with
-      | GCast (c, CastConv, t)
+      | GCast (c, DEFAULTcast, t)
         when isGHole c &&
           let (id, t) = destGLambda t in
           let id = Id.to_string id in let len = String.length id in

plugins/syntax/number.ml

@@ -115,7 +115,7 @@ let locate_int63 () =
   else None
 
 let has_type env sigma f ty =
-  let c = mkCastC (mkRefC f, Glob_term.CastConv, ty) in
+  let c = mkCastC (mkRefC f, Constr.DEFAULTcast, ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
 

plugins/syntax/string_notation.ml

@@ -26,7 +26,7 @@ let q_list () = qualid_of_ref "core.list.type"
 let q_byte () = qualid_of_ref "core.byte.type"
 
 let has_type env sigma f ty =
-  let c = mkCastC (mkRefC f, Glob_term.CastConv, ty) in
+  let c = mkCastC (mkRefC f, Constr.DEFAULTcast, ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
 

pretyping/detyping.ml

@@ -562,7 +562,7 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params
     | CaseInvert {indices} ->
       (* XXX use holes instead of params? *)
       let t = mkApp (mkIndU (ci.ci_ind,univs), Array.append params indices) in
-      DAst.make @@ GCast (tomatch, CastConv, detype t)
+      DAst.make @@ GCast (tomatch, DEFAULTcast, detype t)
   in
   let alias, aliastyp, pred=
     if (not !Flags.raw_print) && synth_type && computable && not (Int.equal (Array.length bl) 0)
@@ -786,12 +786,7 @@ and detype_r d flags avoid env sigma t =
     | Cast (c1,k,c2) ->
       let d1 = detype d flags avoid env sigma c1 in
       let d2 = detype d flags avoid env sigma c2 in
-      let cast = match k with
-        | VMcast -> CastVM
-        | NATIVEcast -> CastNative
-        | DEFAULTcast | REVERTcast -> CastConv
-      in
-      GCast(d1,cast,d2)
+      GCast(d1,k,d2)
     | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma (LocalAssum (na,ty)) c
     | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma (LocalAssum (na,ty)) c
     | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma (LocalDef (na,b,ty)) c

pretyping/glob_ops.ml

@@ -101,11 +101,12 @@ let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
       Name.equal na1 na2
   | (PatVar _ | PatCstr _), _ -> false
 
-let cast_type_eq t1 t2 = match t1, t2 with
-  | CastConv, CastConv
-  | CastVM, CastVM
-  | CastNative, CastNative -> true
-  | (CastConv | CastVM | CastNative), _ -> false
+let cast_kind_eq t1 t2 = let open Constr in match t1, t2 with
+  | DEFAULTcast, DEFAULTcast
+  | REVERTcast, REVERTcast
+  | VMcast, VMcast
+  | NATIVEcast, NATIVEcast -> true
+  | (DEFAULTcast | REVERTcast | VMcast | NATIVEcast), _ -> false
 
 let matching_var_kind_eq k1 k2 = match k1, k2 with
 | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2
@@ -170,7 +171,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Option.equal (==) gn1 gn2 (* Only thing sensible *) &&
     Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, k1, t1), GCast (c2, k2, t2) ->
-    f c1 c2 && cast_type_eq k1 k2 && f t1 t2
+    f c1 c2 && cast_kind_eq k1 k2 && f t1 t2
   | GProj ((cst1, u1), args1, c1), GProj ((cst2, u2), args2, c2) ->
     GlobRef.(equal (ConstRef cst1) (ConstRef cst2)) &&
     Option.equal (List.equal glob_level_eq) u1 u2 &&

pretyping/glob_ops.mli

@@ -32,7 +32,7 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t
 
 val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
 
-val cast_type_eq : cast_type ->  cast_type -> bool
+val cast_kind_eq : Constr.cast_kind ->  Constr.cast_kind -> bool
 
 val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool