Remove redundant keyword escaping fallback and explicit class renames

The lean_reserved_names fallback in backend_common and the explicit
declare {lean} rename type Eq = Eq0 / Ord = Ord0 in basic_classes.lem
were added to work around a Cerberus team build issue (stale object
files). Since rename_top_level already handles keyword escaping via
lean_constants, both mechanisms were redundant.

Keeps: typed_ast_syntax.ml class rename support (genuine infrastructure
fix — declare rename type now works for classes), and the test cases
for prefix/guard/show keyword patterns.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: septract

lean-lib/LemLib/Function.lean

@@ -18,7 +18,7 @@ open Lem_Basic_classes
 /- removed value specification -/
 
 /- 
-def  id0  {a : Type}  (x : a)  : a :=  x -/
+def  id  {a : Type}  (x : a)  : a :=  x -/
 /- removed value specification -/
 
 /- removed top-level value definition -/
@@ -36,7 +36,7 @@ def  rev_apply  {a : Type} {b : Type}  (x : a) (f : a → b)  : b :=  f  x
 /- removed value specification -/
 
 /- 
-def  flip0  {a : Type} {b : Type} {c : Type}  (f : a → b → c)  : b → a → c :=  (fun (x : b) (y : a) =>  f  y  x) -/
+def  flip  {a : Type} {b : Type} {c : Type}  (f : a → b → c)  : b → a → c :=  (fun (x : b) (y : a) =>  f  y  x) -/
 /- removed value specification -/
 
 def  curry  {a : Type} {b : Type} {c : Type}  (f : (a ×b) → c)  : a → b → c :=  (fun (a1 : a) (b1 : b) =>  f  (a1, b1))

library/basic_classes.lem

@@ -23,7 +23,6 @@ class ( Eq 'a )
   val (=) [`isEqual`] : 'a -> 'a -> bool
   val (<>) [`isInequal`] : 'a -> 'a -> bool
 end
-declare {lean} rename type Eq = Eq0
 
 declare coq target_rep function isEqual = infix `=`
 declare lean target_rep function isEqual = infix `==`
@@ -157,7 +156,6 @@ class ( Ord 'a )
   val (>)  [`isGreater`]      : 'a -> 'a -> bool
   val (>=) [`isGreaterEqual`] : 'a -> 'a -> bool
 end
-declare {lean} rename type Ord = Ord0
 
 declare coq target_rep function isLess = `isLess`
 declare coq target_rep function isLessEqual = `isLessEqual`

src/backend_common.ml

@@ -373,18 +373,6 @@ let imported_modules_to_strings env target dir iml relative =
    for non-library target reps only. *)
 let on_cr_simple_applied : (bool -> string -> unit) ref = ref (fun _ _ -> ())
 
-(* Lean reserved names fallback. When rename_top_level doesn't fire
-   (e.g., due to build environment issues), the backend can still
-   escape names by appending "0". Set by lean_backend.ml at startup. *)
-let lean_reserved_names : NameSet.t ref = ref NameSet.empty
-
-(* Check if a name needs escaping for Lean and apply the "0" suffix.
-   Used as a fallback when type_rename/class_rename/target_rename is empty. *)
-let lean_escape_reserved (n : Name.t) : Name.t =
-  if NameSet.mem n !lean_reserved_names then
-    Name.from_string (String.concat "" [Name.to_string n; "0"])
-  else n
-
 module Make(A : sig
   val env : env;;
   val target : Target.target;;
@@ -453,8 +441,6 @@ let const_ref_to_name n0 use_ascii c =
       | (Some ascii, true) -> ascii
       | _  -> n_no_ascii
   in
-  (* Fallback: if rename_top_level didn't fire, check lean_reserved_names *)
-  let n = lean_escape_reserved n in
   let n' = Name.replace_lskip (Name.add_lskip n) (Name.get_lskip n0) in
   n'
 
@@ -599,8 +585,6 @@ let type_path_to_name n0 (p : Path.t) : Name.lskips_t =
   let l = Ast.Trans (false, "type_path_to_name", None) in
   let td = Types.type_defs_lookup l A.env.t_env p in
   let n = type_descr_to_name A.target p td in
-  (* Fallback: if rename_top_level didn't fire, check lean_reserved_names *)
-  let n = lean_escape_reserved n in
   let n' = Name.replace_lskip (Name.add_lskip n) (Name.get_lskip n0) in
   n'
 
@@ -609,9 +593,9 @@ let class_path_to_name (p : Path.t) : Name.t =
     | Some (Types.Tc_class cd) ->
         begin match Target.Targetmap.apply_target cd.Types.class_rename A.target with
           | Some (_, n) -> n
-          | None -> lean_escape_reserved (Path.get_name p)
+          | None -> Path.get_name p
         end
-    | _ -> lean_escape_reserved (Path.get_name p)
+    | _ -> Path.get_name p
 
 let type_id_to_ident_aux (p : Path.t id) =
    let l = Ast.Trans (false, "type_id_to_ident", None) in

src/backend_common.mli

@@ -112,11 +112,6 @@ val imported_modules_to_strings : env -> Target.target -> string -> Imported_Mod
     Set by the Lean backend to collect per-file import requirements. *)
 val on_cr_simple_applied : (bool -> string -> unit) ref
 
-(** Lean reserved names fallback. When rename_top_level doesn't fire,
-    the backend escapes names that collide with Lean keywords by
-    appending "0". Set by lean_backend.ml at startup from lean_constants. *)
-val lean_reserved_names : Typed_ast.NameSet.t ref
-
 module Make(A : sig
   val env : env;;
   val target : Target.target;;

src/main.ml

@@ -277,8 +277,6 @@ end
 
 let transform_for_target libpath modules env targ =
   let consts = Initial_env.read_target_constants libpath targ in
-  (* Make reserved names available to backend_common for fallback escaping *)
-  Backend_common.lean_reserved_names := consts;
 
   let _ = check_env_for_target targ env in