diff --git a/src/proto_alpha/lib_plugin/RPC.ml b/src/proto_alpha/lib_plugin/RPC.ml
index dd9c58546ded1363bb253e5ac59a241bc13a5715..7550c231055b2647d76bce612684c6b6b392c56a 100644
--- a/src/proto_alpha/lib_plugin/RPC.ml
+++ b/src/proto_alpha/lib_plugin/RPC.ml
@@ -2324,9 +2324,8 @@ module Forge = struct
         return (Tx_rollup_withdraw_list_hash.hash_uncarbonated withdrawals))
 
   module Manager = struct
-    let[@coq_axiom_with_reason "cast on e"] operations ctxt block ~branch
-        ~source ?sourcePubKey ~counter ~fee ~gas_limit ~storage_limit operations
-        =
+    let operations ctxt block ~branch ~source ?sourcePubKey ~counter ~fee
+        ~gas_limit ~storage_limit operations =
       Contract_services.manager_key ctxt block source >>= function
       | Error _ as e -> Lwt.return e
       | Ok revealed ->
diff --git a/src/proto_alpha/lib_protocol/apply.ml b/src/proto_alpha/lib_protocol/apply.ml
index 3462c7fb0d97a24d59a7a2a42a971948946e78ae..09b24a16634fc158de6401e2991b55badba905d8 100644
--- a/src/proto_alpha/lib_protocol/apply.ml
+++ b/src/proto_alpha/lib_protocol/apply.ml
@@ -1884,7 +1884,7 @@ let apply_external_manager_operation_content :
 type success_or_failure = Success of context | Failure
 
 let apply_internal_manager_operations ctxt mode ~payer ~chain_id ops =
-  let[@coq_struct "ctxt"] rec apply ctxt applied worklist =
+  let rec apply ctxt applied worklist =
     match worklist with
     | [] -> Lwt.return (Success ctxt, List.rev applied)
     | Script_typed_ir.Internal_operation ({source; operation; nonce} as op)
@@ -2146,14 +2146,7 @@ let apply_manager_contents (type kind) ctxt mode chain_id
     * kind manager_operation_result
     * packed_internal_manager_operation_result list)
     Lwt.t =
-  let[@coq_match_with_default] (Manager_operation
-                                 {
-                                   source;
-                                   operation;
-                                   gas_limit;
-                                   storage_limit;
-                                   _;
-                                 }) =
+  let (Manager_operation {source; operation; gas_limit; storage_limit; _}) =
     op
   in
   (* We do not expose the internal scaling to the users. Instead, we multiply
@@ -2239,7 +2232,7 @@ let rec mark_skipped :
     kind Kind.manager fees_updated_contents_list ->
     kind Kind.manager contents_result_list =
  fun ~payload_producer level fees_updated_contents_list ->
-  match[@coq_match_with_default] fees_updated_contents_list with
+  match fees_updated_contents_list with
   | FeesUpdatedSingle
       {contents = Manager_operation {operation; _}; balance_updates} ->
       Single_result
@@ -2318,7 +2311,7 @@ let rec apply_manager_contents_list_rec :
     (success_or_failure * kind Kind.manager contents_result_list) Lwt.t =
  fun ctxt mode ~payload_producer chain_id fees_updated_contents_list ->
   let level = Level.current ctxt in
-  match[@coq_match_with_default] fees_updated_contents_list with
+  match fees_updated_contents_list with
   | FeesUpdatedSingle {contents = Manager_operation _ as op; balance_updates} ->
       apply_manager_contents ctxt mode chain_id op
       >|= fun (ctxt_result, operation_result, internal_operation_results) ->
@@ -2864,7 +2857,7 @@ let apply_contents_list (type kind) ctxt chain_id (apply_mode : apply_mode) mode
     | Partial_construction _ -> true
     | Full_construction _ | Application _ -> false
   in
-  match[@coq_match_with_default] contents_list with
+  match contents_list with
   | Single (Preendorsement consensus_content) ->
       validate_consensus_contents
         ctxt
diff --git a/src/proto_alpha/lib_protocol/apply_internal_results.ml b/src/proto_alpha/lib_protocol/apply_internal_results.ml
index 01dc7fd8a2daf87bb6bce80b50839b77429e3ecf..5c411a68cf55ad176dd5c7ae5d509103b20cb90a 100644
--- a/src/proto_alpha/lib_protocol/apply_internal_results.ml
+++ b/src/proto_alpha/lib_protocol/apply_internal_results.ml
@@ -216,7 +216,7 @@ module Internal_result = struct
         -> 'kind case
   [@@coq_force_gadt]
 
-  let[@coq_axiom_with_reason "gadt"] transaction_contract_variant_cases =
+  let transaction_contract_variant_cases =
     union
       [
         case
@@ -329,7 +329,7 @@ module Internal_result = struct
           (fun consumed_gas -> Transaction_to_event_result {consumed_gas});
       ]
 
-  let[@coq_axiom_with_reason "gadt"] transaction_case =
+  let transaction_case =
     MCase
       {
         (* This value should be changed with care: maybe receipts are read by
@@ -374,7 +374,7 @@ module Internal_result = struct
             Transaction {amount; destination; parameters; entrypoint});
       }
 
-  let[@coq_axiom_with_reason "gadt"] origination_case =
+  let origination_case =
     MCase
       {
         (* This value should be changed with care: maybe receipts are read by
@@ -402,7 +402,7 @@ module Internal_result = struct
             Origination {credit; delegate; script});
       }
 
-  let[@coq_axiom_with_reason "gadt"] delegation_case =
+  let delegation_case =
     MCase
       {
         (* This value should be changed with care: maybe receipts are read by
@@ -523,7 +523,7 @@ module Internal_manager_result = struct
     in
     MCase {op_case; encoding; kind; select; proj; inj; t}
 
-  let[@coq_axiom_with_reason "gadt"] transaction_case =
+  let transaction_case =
     make
       ~op_case:Internal_result.transaction_case
       ~encoding:Internal_result.transaction_contract_variant_cases
@@ -535,7 +535,7 @@ module Internal_manager_result = struct
       ~proj:(function ITransaction_result x -> x)
       ~inj:(fun x -> ITransaction_result x)
 
-  let[@coq_axiom_with_reason "gadt"] origination_case =
+  let origination_case =
     make
       ~op_case:Internal_result.origination_case
       ~encoding:
@@ -600,8 +600,7 @@ module Internal_manager_result = struct
             Some op
         | _ -> None)
       ~kind:Kind.Delegation_manager_kind
-      ~proj:(function[@coq_match_with_default]
-        | IDelegation_result {consumed_gas} -> consumed_gas)
+      ~proj:(function IDelegation_result {consumed_gas} -> consumed_gas)
       ~inj:(fun consumed_gas -> IDelegation_result {consumed_gas})
 end
 
diff --git a/src/proto_alpha/lib_protocol/apply_results.ml b/src/proto_alpha/lib_protocol/apply_results.ml
index 824c7b4bdeef6cad794a863b7bf301ed3deb2898..d319a04c38985025116b9a60d8c579928b3d905d 100644
--- a/src/proto_alpha/lib_protocol/apply_results.ml
+++ b/src/proto_alpha/lib_protocol/apply_results.ml
@@ -274,7 +274,7 @@ module Manager_result = struct
     in
     MCase {op_case; encoding; kind; select; proj; inj; t}
 
-  let[@coq_axiom_with_reason "gadt"] reveal_case =
+  let reveal_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.reveal_case
       ~encoding:
@@ -287,7 +287,7 @@ module Manager_result = struct
       ~proj:(function Reveal_result {consumed_gas} -> consumed_gas)
       ~inj:(fun consumed_gas -> Reveal_result {consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] transaction_contract_variant_cases =
+  let transaction_contract_variant_cases =
     union
       [
         case
@@ -400,7 +400,7 @@ module Manager_result = struct
           (fun consumed_gas -> Transaction_to_event_result {consumed_gas});
       ]
 
-  let[@coq_axiom_with_reason "gadt"] transaction_case =
+  let transaction_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.transaction_case
       ~encoding:transaction_contract_variant_cases
@@ -411,7 +411,7 @@ module Manager_result = struct
       ~proj:(function Transaction_result x -> x)
       ~inj:(fun x -> Transaction_result x)
 
-  let[@coq_axiom_with_reason "gadt"] origination_case =
+  let origination_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.origination_case
       ~encoding:
@@ -464,7 +464,7 @@ module Manager_result = struct
             paid_storage_size_diff;
           })
 
-  let[@coq_axiom_with_reason "gadt"] register_global_constant_case =
+  let register_global_constant_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.register_global_constant_case
@@ -498,8 +498,7 @@ module Manager_result = struct
         | Successful_manager_result (Delegation_result _ as op) -> Some op
         | _ -> None)
       ~kind:Kind.Delegation_manager_kind
-      ~proj:(function[@coq_match_with_default]
-        | Delegation_result {consumed_gas} -> consumed_gas)
+      ~proj:(function Delegation_result {consumed_gas} -> consumed_gas)
       ~inj:(fun consumed_gas -> Delegation_result {consumed_gas})
 
   let set_deposits_limit_case =
@@ -517,7 +516,7 @@ module Manager_result = struct
         | Set_deposits_limit_result {consumed_gas} -> consumed_gas)
       ~inj:(fun consumed_gas -> Set_deposits_limit_result {consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_origination_case =
+  let tx_rollup_origination_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.tx_rollup_origination_case
       ~encoding:
@@ -539,7 +538,7 @@ module Manager_result = struct
         Tx_rollup_origination_result
           {balance_updates; consumed_gas; originated_tx_rollup})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_submit_batch_case =
+  let tx_rollup_submit_batch_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.tx_rollup_submit_batch_case
       ~encoding:
@@ -561,7 +560,7 @@ module Manager_result = struct
         Tx_rollup_submit_batch_result
           {balance_updates; consumed_gas; paid_storage_size_diff})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_commit_case =
+  let tx_rollup_commit_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.tx_rollup_commit_case
       ~encoding:
@@ -579,7 +578,7 @@ module Manager_result = struct
       ~inj:(fun (balance_updates, consumed_gas) ->
         Tx_rollup_commit_result {balance_updates; consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_return_bond_case =
+  let tx_rollup_return_bond_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.tx_rollup_return_bond_case
       ~encoding:
@@ -598,7 +597,7 @@ module Manager_result = struct
       ~inj:(fun (balance_updates, consumed_gas) ->
         Tx_rollup_return_bond_result {balance_updates; consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_finalize_commitment_case =
+  let tx_rollup_finalize_commitment_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.tx_rollup_finalize_commitment_case
@@ -622,7 +621,7 @@ module Manager_result = struct
         Tx_rollup_finalize_commitment_result
           {balance_updates; consumed_gas; level})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_remove_commitment_case =
+  let tx_rollup_remove_commitment_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.tx_rollup_remove_commitment_case
@@ -646,7 +645,7 @@ module Manager_result = struct
         Tx_rollup_remove_commitment_result
           {balance_updates; consumed_gas; level})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_rejection_case =
+  let tx_rollup_rejection_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.tx_rollup_rejection_case
       ~encoding:
@@ -665,7 +664,7 @@ module Manager_result = struct
       ~inj:(fun (balance_updates, consumed_gas) ->
         Tx_rollup_rejection_result {balance_updates; consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_dispatch_tickets_case =
+  let tx_rollup_dispatch_tickets_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.tx_rollup_dispatch_tickets_case
@@ -689,7 +688,7 @@ module Manager_result = struct
         Tx_rollup_dispatch_tickets_result
           {balance_updates; consumed_gas; paid_storage_size_diff})
 
-  let[@coq_axiom_with_reason "gadt"] transfer_ticket_case =
+  let transfer_ticket_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.transfer_ticket_case
       ~encoding:
@@ -710,7 +709,7 @@ module Manager_result = struct
         Transfer_ticket_result
           {balance_updates; consumed_gas; paid_storage_size_diff})
 
-  let[@coq_axiom_with_reason "gadt"] dal_publish_slot_header_case =
+  let dal_publish_slot_header_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.dal_publish_slot_header_case
@@ -725,7 +724,7 @@ module Manager_result = struct
       ~kind:Kind.Dal_publish_slot_header_manager_kind
       ~inj:(fun consumed_gas -> Dal_publish_slot_header_result {consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_originate_case =
+  let sc_rollup_originate_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.sc_rollup_originate_case
       ~encoding:
@@ -863,7 +862,7 @@ module Manager_result = struct
         Sc_rollup_execute_outbox_message_result
           {balance_updates; consumed_gas; paid_storage_size_diff})
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_recover_bond_case =
+  let sc_rollup_recover_bond_case =
     make
       ~op_case:Operation.Encoding.Manager_operations.sc_rollup_recover_bond_case
       ~encoding:
@@ -882,7 +881,7 @@ module Manager_result = struct
       ~inj:(fun (balance_updates, consumed_gas) ->
         Sc_rollup_recover_bond_result {balance_updates; consumed_gas})
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_dal_slot_subscribe_case =
+  let sc_rollup_dal_slot_subscribe_case =
     make
       ~op_case:
         Operation.Encoding.Manager_operations.sc_rollup_dal_slot_subscribe_case
@@ -1101,7 +1100,7 @@ module Encoding = struct
       (fun x -> match proj x with None -> None | Some x -> Some ((), x))
       (fun ((), x) -> inj x)
 
-  let[@coq_axiom_with_reason "gadt"] preendorsement_case =
+  let preendorsement_case =
     Case
       {
         op_case = Operation.Encoding.preendorsement_case;
@@ -1129,7 +1128,7 @@ module Encoding = struct
               {balance_updates; delegate; preendorsement_power});
       }
 
-  let[@coq_axiom_with_reason "gadt"] endorsement_case =
+  let endorsement_case =
     Case
       {
         op_case = Operation.Encoding.endorsement_case;
@@ -1154,7 +1153,7 @@ module Encoding = struct
             Endorsement_result {balance_updates; delegate; endorsement_power});
       }
 
-  let[@coq_axiom_with_reason "gadt"] dal_slot_availability_case =
+  let dal_slot_availability_case =
     Case
       {
         op_case = Operation.Encoding.dal_slot_availability_case;
@@ -1172,7 +1171,7 @@ module Encoding = struct
         inj = (fun delegate -> Dal_slot_availability_result {delegate});
       }
 
-  let[@coq_axiom_with_reason "gadt"] seed_nonce_revelation_case =
+  let seed_nonce_revelation_case =
     Case
       {
         op_case = Operation.Encoding.seed_nonce_revelation_case;
@@ -1191,7 +1190,7 @@ module Encoding = struct
         inj = (fun bus -> Seed_nonce_revelation_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] vdf_revelation_case =
+  let vdf_revelation_case =
     Case
       {
         op_case = Operation.Encoding.vdf_revelation_case;
@@ -1209,7 +1208,7 @@ module Encoding = struct
         inj = (fun bus -> Vdf_revelation_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_endorsement_evidence_case =
+  let double_endorsement_evidence_case =
     Case
       {
         op_case = Operation.Encoding.double_endorsement_evidence_case;
@@ -1229,7 +1228,7 @@ module Encoding = struct
         inj = (fun bus -> Double_endorsement_evidence_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_preendorsement_evidence_case =
+  let double_preendorsement_evidence_case =
     Case
       {
         op_case = Operation.Encoding.double_preendorsement_evidence_case;
@@ -1250,7 +1249,7 @@ module Encoding = struct
         inj = (fun bus -> Double_preendorsement_evidence_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_baking_evidence_case =
+  let double_baking_evidence_case =
     Case
       {
         op_case = Operation.Encoding.double_baking_evidence_case;
@@ -1269,7 +1268,7 @@ module Encoding = struct
         inj = (fun bus -> Double_baking_evidence_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] activate_account_case =
+  let activate_account_case =
     Case
       {
         op_case = Operation.Encoding.activate_account_case;
@@ -1288,7 +1287,7 @@ module Encoding = struct
         inj = (fun bus -> Activate_account_result bus);
       }
 
-  let[@coq_axiom_with_reason "gadt"] proposals_case =
+  let proposals_case =
     Case
       {
         op_case = Operation.Encoding.proposals_case;
@@ -1304,7 +1303,7 @@ module Encoding = struct
         inj = (fun () -> Proposals_result);
       }
 
-  let[@coq_axiom_with_reason "gadt"] ballot_case =
+  let ballot_case =
     Case
       {
         op_case = Operation.Encoding.ballot_case;
@@ -1320,7 +1319,7 @@ module Encoding = struct
         inj = (fun () -> Ballot_result);
       }
 
-  let[@coq_axiom_with_reason "gadt"] make_manager_case (type kind)
+  let make_manager_case (type kind)
       (Operation.Encoding.Case op_case :
         kind Kind.manager Operation.Encoding.case)
       (Manager_result.MCase res_case : kind Manager_result.case) mselect =
@@ -1403,7 +1402,7 @@ module Encoding = struct
               });
       }
 
-  let[@coq_axiom_with_reason "gadt"] reveal_case =
+  let reveal_case =
     make_manager_case
       Operation.Encoding.reveal_case
       Manager_result.reveal_case
@@ -1413,7 +1412,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] transaction_case =
+  let transaction_case =
     make_manager_case
       Operation.Encoding.transaction_case
       Manager_result.transaction_case
@@ -1423,7 +1422,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] origination_case =
+  let origination_case =
     make_manager_case
       Operation.Encoding.origination_case
       Manager_result.origination_case
@@ -1433,7 +1432,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] delegation_case =
+  let delegation_case =
     make_manager_case
       Operation.Encoding.delegation_case
       Manager_result.delegation_case
@@ -1443,7 +1442,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] register_global_constant_case =
+  let register_global_constant_case =
     make_manager_case
       Operation.Encoding.register_global_constant_case
       Manager_result.register_global_constant_case
@@ -1455,7 +1454,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] set_deposits_limit_case =
+  let set_deposits_limit_case =
     make_manager_case
       Operation.Encoding.set_deposits_limit_case
       Manager_result.set_deposits_limit_case
@@ -1466,7 +1465,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_origination_case =
+  let tx_rollup_origination_case =
     make_manager_case
       Operation.Encoding.tx_rollup_origination_case
       Manager_result.tx_rollup_origination_case
@@ -1477,7 +1476,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_submit_batch_case =
+  let tx_rollup_submit_batch_case =
     make_manager_case
       Operation.Encoding.tx_rollup_submit_batch_case
       Manager_result.tx_rollup_submit_batch_case
@@ -1488,7 +1487,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_commit_case =
+  let tx_rollup_commit_case =
     make_manager_case
       Operation.Encoding.tx_rollup_commit_case
       Manager_result.tx_rollup_commit_case
@@ -1499,7 +1498,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_return_bond_case =
+  let tx_rollup_return_bond_case =
     make_manager_case
       Operation.Encoding.tx_rollup_return_bond_case
       Manager_result.tx_rollup_return_bond_case
@@ -1510,7 +1509,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_finalize_commitment_case =
+  let tx_rollup_finalize_commitment_case =
     make_manager_case
       Operation.Encoding.tx_rollup_finalize_commitment_case
       Manager_result.tx_rollup_finalize_commitment_case
@@ -1522,7 +1521,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_remove_commitment_case =
+  let tx_rollup_remove_commitment_case =
     make_manager_case
       Operation.Encoding.tx_rollup_remove_commitment_case
       Manager_result.tx_rollup_remove_commitment_case
@@ -1534,7 +1533,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_rejection_case =
+  let tx_rollup_rejection_case =
     make_manager_case
       Operation.Encoding.tx_rollup_rejection_case
       Manager_result.tx_rollup_rejection_case
@@ -1545,7 +1544,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] tx_rollup_dispatch_tickets_case =
+  let tx_rollup_dispatch_tickets_case =
     make_manager_case
       Operation.Encoding.tx_rollup_dispatch_tickets_case
       Manager_result.tx_rollup_dispatch_tickets_case
@@ -1557,7 +1556,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] transfer_ticket_case =
+  let transfer_ticket_case =
     make_manager_case
       Operation.Encoding.transfer_ticket_case
       Manager_result.transfer_ticket_case
@@ -1568,7 +1567,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] dal_publish_slot_header_case =
+  let dal_publish_slot_header_case =
     make_manager_case
       Operation.Encoding.dal_publish_slot_header_case
       Manager_result.dal_publish_slot_header_case
@@ -1580,7 +1579,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_originate_case =
+  let sc_rollup_originate_case =
     make_manager_case
       Operation.Encoding.sc_rollup_originate_case
       Manager_result.sc_rollup_originate_case
@@ -1591,7 +1590,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_add_messages_case =
+  let sc_rollup_add_messages_case =
     make_manager_case
       Operation.Encoding.sc_rollup_add_messages_case
       Manager_result.sc_rollup_add_messages_case
@@ -1602,7 +1601,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_cement_case =
+  let sc_rollup_cement_case =
     make_manager_case
       Operation.Encoding.sc_rollup_cement_case
       Manager_result.sc_rollup_cement_case
@@ -1613,7 +1612,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_publish_case =
+  let sc_rollup_publish_case =
     make_manager_case
       Operation.Encoding.sc_rollup_publish_case
       Manager_result.sc_rollup_publish_case
@@ -1624,7 +1623,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_refute_case =
+  let sc_rollup_refute_case =
     make_manager_case
       Operation.Encoding.sc_rollup_refute_case
       Manager_result.sc_rollup_refute_case
@@ -1635,7 +1634,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_timeout_case =
+  let sc_rollup_timeout_case =
     make_manager_case
       Operation.Encoding.sc_rollup_timeout_case
       Manager_result.sc_rollup_timeout_case
@@ -1646,7 +1645,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_execute_outbox_message_case =
+  let sc_rollup_execute_outbox_message_case =
     make_manager_case
       Operation.Encoding.sc_rollup_execute_outbox_message_case
       Manager_result.sc_rollup_execute_outbox_message_case
@@ -1658,7 +1657,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_recover_bond_case =
+  let sc_rollup_recover_bond_case =
     make_manager_case
       Operation.Encoding.sc_rollup_recover_bond_case
       Manager_result.sc_rollup_recover_bond_case
@@ -1669,7 +1668,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] sc_rollup_dal_slot_subscribe_case =
+  let sc_rollup_dal_slot_subscribe_case =
     make_manager_case
       Operation.Encoding.sc_rollup_dal_slot_subscribe_case
       Manager_result.sc_rollup_dal_slot_subscribe_case
@@ -2618,7 +2617,7 @@ let rec kind_equal_list :
           | Some Eq -> Some Eq))
   | _ -> None
 
-let[@coq_axiom_with_reason "gadt"] rec pack_contents_list :
+let rec pack_contents_list :
     type kind.
     kind contents_list ->
     kind contents_result_list ->
diff --git a/src/proto_alpha/lib_protocol/contract_repr.ml b/src/proto_alpha/lib_protocol/contract_repr.ml
index 20045646df690fe5c0afcf1436361b5434357fe2..fd9fb7ca3f1bfb021e0252f9124948596b8ac974 100644
--- a/src/proto_alpha/lib_protocol/contract_repr.ml
+++ b/src/proto_alpha/lib_protocol/contract_repr.ml
@@ -190,7 +190,7 @@ let originated_contracts
       (Origination_nonce.{origination_index = last; operation_hash = last_hash}
       as origination_nonce) =
   assert (Operation_hash.equal first_hash last_hash) ;
-  let[@coq_struct "origination_index"] rec contracts acc origination_index =
+  let rec contracts acc origination_index =
     if Compare.Int32.(origination_index < first) then acc
     else
       let origination_nonce = {origination_nonce with origination_index} in
diff --git a/src/proto_alpha/lib_protocol/contract_services.ml b/src/proto_alpha/lib_protocol/contract_services.ml
index 1d18c7117acf7f67d9e50a1486d620f6adda6818..f067f3b48e3b42dbb564059a1389e6a1550daff8 100644
--- a/src/proto_alpha/lib_protocol/contract_services.ml
+++ b/src/proto_alpha/lib_protocol/contract_services.ml
@@ -290,7 +290,7 @@ module S = struct
   end
 end
 
-let[@coq_axiom_with_reason "gadt"] register () =
+let register () =
   let open Services_registration in
   register0 ~chunked:true S.list (fun ctxt () () -> Contract.list ctxt >|= ok) ;
   let register_field_gen ~filter_contract ~wrap_result ~chunked s f =
diff --git a/src/proto_alpha/lib_protocol/level_storage.ml b/src/proto_alpha/lib_protocol/level_storage.ml
index 852e8a84899b925b0d360231ccdd43d11da958fe..e1838c9d9912535dae40e184a7915261aca64572 100644
--- a/src/proto_alpha/lib_protocol/level_storage.ml
+++ b/src/proto_alpha/lib_protocol/level_storage.ml
@@ -73,7 +73,7 @@ let last_level_in_cycle ctxt c =
 
 let levels_in_cycle ctxt cycle =
   let first = first_level_in_cycle ctxt cycle in
-  let[@coq_struct "n"] rec loop (n : Level_repr.t) acc =
+  let rec loop (n : Level_repr.t) acc =
     if Cycle_repr.(n.cycle = first.cycle) then loop (succ ctxt n) (n :: acc)
     else acc
   in
@@ -89,7 +89,7 @@ let levels_in_current_cycle ctxt ?(offset = 0l) () =
 
 let levels_with_commitments_in_cycle ctxt c =
   let first = first_level_in_cycle ctxt c in
-  let[@coq_struct "n"] rec loop (n : Level_repr.t) acc =
+  let rec loop (n : Level_repr.t) acc =
     if Cycle_repr.(n.cycle = first.cycle) then
       if n.expected_commitment then loop (succ ctxt n) (n :: acc)
       else loop (succ ctxt n) acc
diff --git a/src/proto_alpha/lib_protocol/main.ml b/src/proto_alpha/lib_protocol/main.ml
index 12ee15cff4cf3f5675ae1029ba6f84c924dda62a..100edf55a0e06d941288e5ebee07feea703e1091 100644
--- a/src/proto_alpha/lib_protocol/main.ml
+++ b/src/proto_alpha/lib_protocol/main.ml
@@ -720,7 +720,7 @@ let relative_position_within_block op1 op2 =
   let open Alpha_context in
   let (Operation_data op1) = op1.protocol_data in
   let (Operation_data op2) = op2.protocol_data in
-  match[@coq_match_with_default] (op1.contents, op2.contents) with
+  match (op1.contents, op2.contents) with
   | Single (Preendorsement _), Single (Preendorsement _) -> 0
   | Single (Preendorsement _), _ -> -1
   | _, Single (Preendorsement _) -> 1
diff --git a/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml b/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml
index abbad29046c1dae6433d9fa3e6f53aa9006f2fcc..eedb5c43d4db1d92fcb9714cde7b687f8d7fa0a3 100644
--- a/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml
+++ b/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml
@@ -232,9 +232,7 @@ let namespace = function
 let valid_case name =
   let is_lower = function '_' | 'a' .. 'z' -> true | _ -> false in
   let is_upper = function '_' | 'A' .. 'Z' -> true | _ -> false in
-  let[@coq_struct "a_value"] rec for_all a b f =
-    Compare.Int.(a > b) || (f a && for_all (a + 1) b f)
-  in
+  let rec for_all a b f = Compare.Int.(a > b) || (f a && for_all (a + 1) b f) in
   let len = String.length name in
   Compare.Int.(len <> 0)
   && Compare.Char.(name.[0] <> '_')
diff --git a/src/proto_alpha/lib_protocol/misc.ml b/src/proto_alpha/lib_protocol/misc.ml
index bd350a5ef85b2a35d204d68f06094db9686e565d..fd19a63ad49795ec211ea87ab3784fde74bb073d 100644
--- a/src/proto_alpha/lib_protocol/misc.ml
+++ b/src/proto_alpha/lib_protocol/misc.ml
@@ -31,15 +31,15 @@ type 'a lazy_list_t = LCons of 'a * 'a lazy_list_t tzresult Lwt.t lazyt
 
 type 'a lazy_list = 'a lazy_list_t tzresult Lwt.t
 
-let[@coq_struct "i"] rec ( --> ) i j =
+let rec ( --> ) i j =
   (* [i; i+1; ...; j] *)
   if Compare.Int.(i > j) then [] else i :: (succ i --> j)
 
-let[@coq_struct "j"] rec ( <-- ) i j =
+let rec ( <-- ) i j =
   (* [j; j-1; ...; i] *)
   if Compare.Int.(i > j) then [] else j :: (i <-- pred j)
 
-let[@coq_struct "i"] rec ( ---> ) i j =
+let rec ( ---> ) i j =
   (* [i; i+1; ...; j] *)
   if Compare.Int32.(i > j) then [] else i :: (Int32.succ i ---> j)
 
diff --git a/src/proto_alpha/lib_protocol/operation_repr.ml b/src/proto_alpha/lib_protocol/operation_repr.ml
index 5501508072a0b6dbaf1f23e868f907a245246c6f..5847eb1fed67f832a13a76f32a2845478755d825 100644
--- a/src/proto_alpha/lib_protocol/operation_repr.ml
+++ b/src/proto_alpha/lib_protocol/operation_repr.ml
@@ -601,7 +601,7 @@ module Encoding = struct
           -> 'kind case
     [@@coq_force_gadt]
 
-    let[@coq_axiom_with_reason "gadt"] reveal_case =
+    let reveal_case =
       MCase
         {
           tag = 0;
@@ -612,7 +612,7 @@ module Encoding = struct
           inj = (fun pkh -> Reveal pkh);
         }
 
-    let[@coq_axiom_with_reason "gadt"] transaction_case =
+    let transaction_case =
       MCase
         {
           tag = 1;
@@ -649,7 +649,7 @@ module Encoding = struct
               Transaction {amount; destination; parameters; entrypoint});
         }
 
-    let[@coq_axiom_with_reason "gadt"] origination_case =
+    let origination_case =
       MCase
         {
           tag = 2;
@@ -670,7 +670,7 @@ module Encoding = struct
               Origination {credit; delegate; script});
         }
 
-    let[@coq_axiom_with_reason "gadt"] delegation_case =
+    let delegation_case =
       MCase
         {
           tag = 3;
@@ -682,7 +682,7 @@ module Encoding = struct
           inj = (fun key -> Delegation key);
         }
 
-    let[@coq_axiom_with_reason "gadt"] register_global_constant_case =
+    let register_global_constant_case =
       MCase
         {
           tag = 4;
@@ -695,7 +695,7 @@ module Encoding = struct
           inj = (fun value -> Register_global_constant {value});
         }
 
-    let[@coq_axiom_with_reason "gadt"] set_deposits_limit_case =
+    let set_deposits_limit_case =
       MCase
         {
           tag = 5;
@@ -708,7 +708,7 @@ module Encoding = struct
           inj = (fun key -> Set_deposits_limit key);
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_origination_case =
+    let tx_rollup_origination_case =
       MCase
         {
           tag = tx_rollup_operation_origination_tag;
@@ -727,7 +727,7 @@ module Encoding = struct
          encoding which is in hexadecimal for JSON. *)
       conv Bytes.of_string Bytes.to_string bytes
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_submit_batch_case =
+    let tx_rollup_submit_batch_case =
       MCase
         {
           tag = tx_rollup_operation_submit_batch_tag;
@@ -749,7 +749,7 @@ module Encoding = struct
               Tx_rollup_submit_batch {tx_rollup; content; burn_limit});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_commit_case =
+    let tx_rollup_commit_case =
       MCase
         {
           tag = tx_rollup_operation_commit_tag;
@@ -769,7 +769,7 @@ module Encoding = struct
               Tx_rollup_commit {tx_rollup; commitment});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_return_bond_case =
+    let tx_rollup_return_bond_case =
       MCase
         {
           tag = tx_rollup_operation_return_bond_tag;
@@ -782,7 +782,7 @@ module Encoding = struct
           inj = (fun tx_rollup -> Tx_rollup_return_bond {tx_rollup});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_finalize_commitment_case =
+    let tx_rollup_finalize_commitment_case =
       MCase
         {
           tag = tx_rollup_operation_finalize_commitment_tag;
@@ -797,7 +797,7 @@ module Encoding = struct
           inj = (fun tx_rollup -> Tx_rollup_finalize_commitment {tx_rollup});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_remove_commitment_case =
+    let tx_rollup_remove_commitment_case =
       MCase
         {
           tag = tx_rollup_operation_remove_commitment_tag;
@@ -812,7 +812,7 @@ module Encoding = struct
           inj = (fun tx_rollup -> Tx_rollup_remove_commitment {tx_rollup});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_rejection_case =
+    let tx_rollup_rejection_case =
       MCase
         {
           tag = tx_rollup_operation_rejection_tag;
@@ -891,7 +891,7 @@ module Encoding = struct
                 });
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_dispatch_tickets_case =
+    let tx_rollup_dispatch_tickets_case =
       MCase
         {
           tag = tx_rollup_operation_dispatch_tickets_tag;
@@ -947,7 +947,7 @@ module Encoding = struct
                 });
         }
 
-    let[@coq_axiom_with_reason "gadt"] transfer_ticket_case =
+    let transfer_ticket_case =
       MCase
         {
           tag = transfer_ticket_tag;
@@ -974,7 +974,7 @@ module Encoding = struct
                 {contents; ty; ticketer; amount; destination; entrypoint});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_originate_case =
+    let sc_rollup_originate_case =
       MCase
         {
           tag = sc_rollup_operation_origination_tag;
@@ -996,7 +996,7 @@ module Encoding = struct
               Sc_rollup_originate {kind; boot_sector; parameters_ty});
         }
 
-    let[@coq_axiom_with_reason "gadt"] dal_publish_slot_header_case =
+    let dal_publish_slot_header_case =
       MCase
         {
           tag = dal_publish_slot_header_tag;
@@ -1009,7 +1009,7 @@ module Encoding = struct
           inj = (fun slot -> Dal_publish_slot_header {slot});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_add_messages_case =
+    let sc_rollup_add_messages_case =
       MCase
         {
           tag = sc_rollup_operation_add_message_tag;
@@ -1029,7 +1029,7 @@ module Encoding = struct
               Sc_rollup_add_messages {rollup; messages});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_cement_case =
+    let sc_rollup_cement_case =
       MCase
         {
           tag = sc_rollup_operation_cement_tag;
@@ -1048,7 +1048,7 @@ module Encoding = struct
             (fun (rollup, commitment) -> Sc_rollup_cement {rollup; commitment});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_publish_case =
+    let sc_rollup_publish_case =
       MCase
         {
           tag = sc_rollup_operation_publish_tag;
@@ -1067,7 +1067,7 @@ module Encoding = struct
             (fun (rollup, commitment) -> Sc_rollup_publish {rollup; commitment});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_refute_case =
+    let sc_rollup_refute_case =
       MCase
         {
           tag = sc_rollup_operation_refute_tag;
@@ -1091,7 +1091,7 @@ module Encoding = struct
               Sc_rollup_refute {rollup; opponent; refutation});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_timeout_case =
+    let sc_rollup_timeout_case =
       MCase
         {
           tag = sc_rollup_operation_timeout_tag;
@@ -1109,7 +1109,7 @@ module Encoding = struct
           inj = (fun (rollup, stakers) -> Sc_rollup_timeout {rollup; stakers});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_execute_outbox_message_case =
+    let sc_rollup_execute_outbox_message_case =
       MCase
         {
           tag = sc_rollup_execute_outbox_message_tag;
@@ -1136,7 +1136,7 @@ module Encoding = struct
                 {rollup; cemented_commitment; output_proof});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_recover_bond_case =
+    let sc_rollup_recover_bond_case =
       MCase
         {
           tag = sc_rollup_operation_recover_bond_tag;
@@ -1149,7 +1149,7 @@ module Encoding = struct
           inj = (fun sc_rollup -> Sc_rollup_recover_bond {sc_rollup});
         }
 
-    let[@coq_axiom_with_reason "gadt"] sc_rollup_dal_slot_subscribe_case =
+    let sc_rollup_dal_slot_subscribe_case =
       MCase
         {
           tag = sc_rollup_operation_dal_slot_subscribe_tag;
@@ -1237,7 +1237,7 @@ module Encoding = struct
         select =
           (function Contents (Endorsement _ as op) -> Some op | _ -> None);
         proj =
-          (fun [@coq_match_with_default] (Endorsement consensus_content) ->
+          (fun (Endorsement consensus_content) ->
             ( consensus_content.slot,
               consensus_content.level,
               consensus_content.round,
@@ -1247,7 +1247,7 @@ module Encoding = struct
             Endorsement {slot; level; round; block_payload_hash});
       }
 
-  let[@coq_axiom_with_reason "gadt"] endorsement_encoding =
+  let endorsement_encoding =
     let make (Case {tag; name; encoding; select = _; proj; inj}) =
       case (Tag tag) name encoding (fun o -> Some (proj o)) (fun x -> inj x)
     in
@@ -1284,15 +1284,14 @@ module Encoding = struct
           (function
           | Contents (Dal_slot_availability _ as op) -> Some op | _ -> None);
         proj =
-          (fun [@coq_match_with_default] (Dal_slot_availability
-                                           (endorser, endorsement)) ->
+          (fun (Dal_slot_availability (endorser, endorsement)) ->
             (endorser, endorsement));
         inj =
           (fun (endorser, endorsement) ->
             Dal_slot_availability (endorser, endorsement));
       }
 
-  let[@coq_axiom_with_reason "gadt"] seed_nonce_revelation_case =
+  let seed_nonce_revelation_case =
     Case
       {
         tag = 1;
@@ -1308,7 +1307,7 @@ module Encoding = struct
         inj = (fun (level, nonce) -> Seed_nonce_revelation {level; nonce});
       }
 
-  let[@coq_axiom_with_reason "gadt"] vdf_revelation_case =
+  let vdf_revelation_case =
     Case
       {
         tag = 8;
@@ -1320,7 +1319,7 @@ module Encoding = struct
         inj = (fun solution -> Vdf_revelation {solution});
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_preendorsement_evidence_case :
+  let double_preendorsement_evidence_case :
       Kind.double_preendorsement_evidence case =
     Case
       {
@@ -1338,8 +1337,7 @@ module Encoding = struct
         inj = (fun (op1, op2) -> Double_preendorsement_evidence {op1; op2});
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_endorsement_evidence_case :
-      Kind.double_endorsement_evidence case =
+  let double_endorsement_evidence_case : Kind.double_endorsement_evidence case =
     Case
       {
         tag = 2;
@@ -1356,7 +1354,7 @@ module Encoding = struct
         inj = (fun (op1, op2) -> Double_endorsement_evidence {op1; op2});
       }
 
-  let[@coq_axiom_with_reason "gadt"] double_baking_evidence_case =
+  let double_baking_evidence_case =
     Case
       {
         tag = 3;
@@ -1372,7 +1370,7 @@ module Encoding = struct
         inj = (fun (bh1, bh2) -> Double_baking_evidence {bh1; bh2});
       }
 
-  let[@coq_axiom_with_reason "gadt"] activate_account_case =
+  let activate_account_case =
     Case
       {
         tag = 4;
@@ -1391,7 +1389,7 @@ module Encoding = struct
           (fun (id, activation_code) -> Activate_account {id; activation_code});
       }
 
-  let[@coq_axiom_with_reason "gadt"] proposals_case =
+  let proposals_case =
     Case
       {
         tag = 5;
@@ -1411,7 +1409,7 @@ module Encoding = struct
             Proposals {source; period; proposals});
       }
 
-  let[@coq_axiom_with_reason "gadt"] ballot_case =
+  let ballot_case =
     Case
       {
         tag = 6;
@@ -1440,8 +1438,7 @@ module Encoding = struct
         encoding = obj1 (req "arbitrary" Data_encoding.string);
         select =
           (function Contents (Failing_noop _ as op) -> Some op | _ -> None);
-        proj =
-          (function[@coq_match_with_default] Failing_noop message -> message);
+        proj = (function Failing_noop message -> message);
         inj = (function message -> Failing_noop message);
       }
 
@@ -1453,8 +1450,7 @@ module Encoding = struct
       (req "gas_limit" (check_size 10 Gas_limit_repr.Arith.n_integral_encoding))
       (req "storage_limit" (check_size 10 n))
 
-  let extract : type kind. kind Kind.manager contents -> _ =
-    function[@coq_match_with_default]
+  let extract : type kind. kind Kind.manager contents -> _ = function
     | Manager_operation
         {source; fee; counter; gas_limit; storage_limit; operation = _} ->
         (source, fee, counter, gas_limit, storage_limit)
@@ -1463,7 +1459,7 @@ module Encoding = struct
     Manager_operation
       {source; fee; counter; gas_limit; storage_limit; operation}
 
-  let[@coq_axiom_with_reason "gadt"] make_manager_case tag (type kind)
+  let make_manager_case tag (type kind)
       (Manager_operations.MCase mcase : kind Manager_operations.case) =
     Case
       {
diff --git a/src/proto_alpha/lib_protocol/sapling_storage.ml b/src/proto_alpha/lib_protocol/sapling_storage.ml
index 3f151b75784725fc27024965b1aad5d2ae943e85..e043a080a46f5df6467c2a743707743beab47e03 100644
--- a/src/proto_alpha/lib_protocol/sapling_storage.ml
+++ b/src/proto_alpha/lib_protocol/sapling_storage.ml
@@ -149,7 +149,7 @@ module Commitments : COMMITMENTS = struct
           pos = size tree /\
      Post: incremental tree /\
            to_list (insert tree height pos cms) = to_list t @ cms *)
-  let[@coq_struct "height"] rec insert ctx id node height pos cms =
+  let rec insert ctx id node height pos cms =
     assert_node node height ;
     assert_height height ;
     assert_pos pos height ;
@@ -178,8 +178,7 @@ module Commitments : COMMITMENTS = struct
         Storage.Sapling.Commitments.add (ctx, id) node h
         >|=? fun (ctx, size, _existing) -> (ctx, size + size_children, h)
 
-  let[@coq_struct "height"] rec fold_from_height ctx id node ~pos ~f ~acc height
-      =
+  let rec fold_from_height ctx id node ~pos ~f ~acc height =
     assert_node node height ;
     assert_height height ;
     assert_pos pos height ;
@@ -279,7 +278,7 @@ module Nullifiers = struct
     (ctx, size)
 
   let get_from ctx id offset =
-    let[@coq_struct "pos"] rec aux acc pos =
+    let rec aux acc pos =
       Storage.Sapling.Nullifiers_ordered.find (ctx, id) pos >>=? function
       | None -> return @@ List.rev acc
       | Some c -> aux (c :: acc) (Int64.succ pos)
@@ -306,7 +305,7 @@ module Roots = struct
     Storage.Sapling.Roots.get (ctx, id) pos
 
   let init ctx id =
-    let[@coq_struct "pos"] rec aux ctx pos =
+    let rec aux ctx pos =
       if Compare.Int32.(pos < 0l) then return ctx
       else
         Storage.Sapling.Roots.init (ctx, id) pos Commitments.default_root
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 15ff0c35128189fe791969f6e98ec0b49c4cd51f..9fbfed805ad9fc8948f2aed907a151320a51b228 100644
--- a/src/proto_alpha/lib_protocol/script_ir_translator.ml
+++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml
@@ -291,7 +291,7 @@ let serialize_ty_for_error ty =
   *)
   unparse_ty_uncarbonated ~loc:() ty |> Micheline.strip_locations
 
-let[@coq_axiom_with_reason "gadt"] check_comparable :
+let check_comparable :
     type a ac.
     Script.location -> (a, ac) ty -> (ac, Dependent_bool.yes) eq tzresult =
  fun loc ty ->
@@ -521,7 +521,7 @@ let comb_witness2 :
   | Pair_t _ -> Comb_Pair Comb_Any
   | _ -> Comb_Any
 
-let[@coq_axiom_with_reason "gadt"] rec unparse_comparable_data :
+let rec unparse_comparable_data :
     type a loc.
     loc:loc ->
     context ->
@@ -938,7 +938,7 @@ let parse_memo_size (n : (location, _) Micheline.node) :
   match n with
   | Int (_, z) -> (
       match Sapling.Memo_size.parse_z z with
-      | Ok _ as ok_memo_size -> ok_memo_size [@coq_cast]
+      | Ok _ as ok_memo_size -> ok_memo_size
       | Error msg ->
           error
           @@ Invalid_syntactic_constant (location n, strip_locations n, msg))
@@ -970,7 +970,7 @@ type ('ret, 'name) parse_ty_ret =
   | Parse_entrypoints
       : (ex_parameter_ty_and_entrypoints_node, Entrypoint.t option) parse_ty_ret
 
-let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty :
+let rec parse_ty :
     type ret name.
     context ->
     stack_depth:int ->
@@ -1310,8 +1310,7 @@ let[@coq_axiom_with_reason "complex mutually recursive definition"] rec parse_ty
                T_unit;
              ]
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_comparable_ty
-    :
+and parse_comparable_ty :
     context ->
     stack_depth:int ->
     Script.node ->
@@ -1334,7 +1333,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_compar
       error
         (Comparable_type_expected (location node, Micheline.strip_locations node))
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_passable_ty :
+and parse_passable_ty :
     type ret name.
     context ->
     stack_depth:int ->
@@ -1352,8 +1351,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_passab
     ~allow_contract:true
     ~allow_ticket:true
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_any_ty
-    :
+and parse_any_ty :
     context ->
     stack_depth:int ->
     legacy:bool ->
@@ -1370,8 +1368,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_any_ty
     ~allow_ticket:true
     ~ret:Don't_parse_entrypoints
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_big_map_ty
-    ctxt ~stack_depth ~legacy big_map_loc args map_annot =
+and parse_big_map_ty ctxt ~stack_depth ~legacy big_map_loc args map_annot =
   Gas.consume ctxt Typecheck_costs.parse_type_cycle >>? fun ctxt ->
   match args with
   | [key_ty; value_ty] ->
@@ -1388,8 +1385,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_big_ma
       (Ex_ty big_map_ty, ctxt)
   | args -> error @@ Invalid_arity (big_map_loc, T_big_map, 2, List.length args)
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_big_map_value_ty
-    ctxt ~stack_depth ~legacy value_ty =
+and parse_big_map_value_ty ctxt ~stack_depth ~legacy value_ty =
   (parse_ty [@tailcall])
     ctxt
     ~stack_depth
@@ -2306,7 +2302,7 @@ let parse_toplevel :
   - storage after origination
 *)
 
-let[@coq_axiom_with_reason "gadt"] rec parse_data :
+let rec parse_data :
     type a ac.
     ?type_logger:type_logger ->
     stack_depth:int ->
@@ -2829,7 +2825,7 @@ and parse_views :
   in
   Script_map.map_es_in_context aux ctxt views
 
-and[@coq_axiom_with_reason "gadt"] parse_returning :
+and parse_returning :
     type arg argc ret retc.
     ?type_logger:type_logger ->
     stack_depth:int ->
@@ -2872,7 +2868,7 @@ and[@coq_axiom_with_reason "gadt"] parse_returning :
             : (arg, ret) lambda),
           ctxt )
 
-and[@coq_axiom_with_reason "gadt"] parse_instr :
+and parse_instr :
     type a s.
     ?type_logger:type_logger ->
     stack_depth:int ->
@@ -4854,7 +4850,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr :
              I_XOR;
            ]
 
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contract_data :
+and parse_contract_data :
     type arg argc.
     stack_depth:int ->
     context ->
@@ -4886,7 +4882,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra
    The inner [result] is turned into an [option] by [parse_contract_for_script].
    Both [tzresult] are merged by [parse_contract_data].
 *)
-and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contract :
+and parse_contract :
     type arg argc err.
     stack_depth:int ->
     context ->
@@ -5128,7 +5124,7 @@ let parse_storage :
        storage_type
        (root storage))
 
-let[@coq_axiom_with_reason "gadt"] parse_script :
+let parse_script :
     ?type_logger:type_logger ->
     context ->
     legacy:bool ->
@@ -5274,7 +5270,7 @@ let list_entrypoints_uncarbonated (type full fullc) (full : (full, fullc) ty)
 
 (* -- Unparsing data of any type -- *)
 
-let[@coq_axiom_with_reason "gadt"] rec unparse_data :
+let rec unparse_data :
     type a ac.
     context ->
     stack_depth:int ->
@@ -5478,7 +5474,7 @@ and unparse_items :
     ([], ctxt)
     items
 
-and[@coq_axiom_with_reason "gadt"] unparse_code ctxt ~stack_depth mode code =
+and unparse_code ctxt ~stack_depth mode code =
   let legacy = true in
   Gas.consume ctxt Unparse_costs.unparse_instr_cycle >>?= fun ctxt ->
   let non_terminal_recursion ctxt mode code =
@@ -5797,8 +5793,7 @@ let rec has_lazy_storage : type t tc. (t, tc) ty -> t has_lazy_storage =
   storage diff to show on the receipt and apply on the storage.
 
 *)
-let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode
-    ~temporary ids_to_copy acc ty x =
+let extract_lazy_storage_updates ctxt mode ~temporary ids_to_copy acc ty x =
   let rec aux :
       type a ac.
       context ->
@@ -5909,7 +5904,7 @@ end
 (** Prematurely abort if [f] generates an error. Use this function without the
     [unit] type for [error] if you are in a case where errors are impossible.
 *)
-let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage :
+let rec fold_lazy_storage :
     type a ac error.
     f:('acc, error) Fold_lazy_storage.result Lazy_storage.IdSet.fold_f ->
     init:'acc ->
@@ -5968,7 +5963,7 @@ let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage :
         m
         (ok (Fold_lazy_storage.Ok init, ctxt))
 
-let[@coq_axiom_with_reason "gadt"] collect_lazy_storage ctxt ty x =
+let collect_lazy_storage ctxt ty x =
   let has_lazy_storage = has_lazy_storage ty in
   let f kind id (acc : (_, never) Fold_lazy_storage.result) =
     let acc = match acc with Fold_lazy_storage.Ok acc -> acc in
@@ -5978,8 +5973,8 @@ let[@coq_axiom_with_reason "gadt"] collect_lazy_storage ctxt ty x =
   >>? fun (ids, ctxt) ->
   match ids with Fold_lazy_storage.Ok ids -> ok (ids, ctxt)
 
-let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_diff ctxt mode
-    ~temporary ~to_duplicate ~to_update ty v =
+let extract_lazy_storage_diff ctxt mode ~temporary ~to_duplicate ~to_update ty v
+    =
   (*
     Basically [to_duplicate] are ids from the argument and [to_update] are ids
     from the storage before execution (i.e. it is safe to reuse them since they
@@ -6056,7 +6051,7 @@ let parse_ty = parse_ty ~stack_depth:0 ~ret:Don't_parse_entrypoints
 let parse_parameter_ty_and_entrypoints =
   parse_parameter_ty_and_entrypoints ~stack_depth:0
 
-let[@coq_axiom_with_reason "gadt"] get_single_sapling_state ctxt ty x =
+let get_single_sapling_state ctxt ty x =
   let has_lazy_storage = has_lazy_storage ty in
   let f (type i a u) (kind : (i, a, u) Lazy_storage.Kind.t) (id : i)
       single_id_opt : (Sapling.Id.t option, unit) Fold_lazy_storage.result =
diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml
index 681d6d7c627a54161e667a89f2aa46381efff12d..d47eee936e96f8a19202554fa14645daea3e85d0 100644
--- a/src/proto_alpha/lib_protocol/script_repr.ml
+++ b/src/proto_alpha/lib_protocol/script_repr.ml
@@ -117,7 +117,7 @@ module Micheline_size = struct
   let of_annots acc annots =
     List.fold_left (fun acc s -> add_string acc s) acc annots
 
-  let[@coq_struct "nodes"] rec of_nodes acc nodes more_nodes =
+  let rec of_nodes acc nodes more_nodes =
     let open Micheline in
     match nodes with
     | [] -> (
@@ -312,7 +312,7 @@ let is_unit_parameter =
     ~fun_bytes:(fun b -> Compare.Bytes.equal b unit_bytes)
     ~fun_combine:(fun res _ -> res)
 
-let[@coq_struct "node"] rec strip_annotations node =
+let rec strip_annotations node =
   let open Micheline in
   match node with
   | (Int (_, _) | String (_, _) | Bytes (_, _)) as leaf -> leaf
@@ -330,8 +330,7 @@ let rec micheline_fold_aux node f acc k =
   | Micheline.Seq (_, subterms) ->
       micheline_fold_nodes subterms f (f acc node) k
 
-and[@coq_mutual_as_notation] [@coq_struct "subterms"] micheline_fold_nodes
-    subterms f acc k =
+and micheline_fold_nodes subterms f acc k =
   match subterms with
   | [] -> k acc
   | node :: nodes ->
diff --git a/src/proto_alpha/lib_protocol/seed_repr.ml b/src/proto_alpha/lib_protocol/seed_repr.ml
index 23dc8fe39f521bea333b0de621164d736030bed1..f06d2fe82dd354687ec521f60652c3c814ed9805 100644
--- a/src/proto_alpha/lib_protocol/seed_repr.ml
+++ b/src/proto_alpha/lib_protocol/seed_repr.ml
@@ -215,7 +215,7 @@ let initial_nonce_hash_0 = hash initial_nonce_0
 let deterministic_seed seed = update_seed seed zero_bytes
 
 let initial_seeds ?initial_seed n =
-  let[@coq_struct "i"] rec loop acc elt i =
+  let rec loop acc elt i =
     if Compare.Int.(i = 1) then List.rev (elt :: acc)
     else loop (elt :: acc) (deterministic_seed elt) (i - 1)
   in
diff --git a/src/proto_alpha/lib_protocol/storage_description.ml b/src/proto_alpha/lib_protocol/storage_description.ml
index 86aed867ac16187268cf940550636bb291a6f689..e659f6b82cecd2c9247e3b877827ad055a9aba4b 100644
--- a/src/proto_alpha/lib_protocol/storage_description.ml
+++ b/src/proto_alpha/lib_protocol/storage_description.ml
@@ -56,8 +56,7 @@ and 'key description =
     }
       -> 'key description
 
-let[@coq_struct "function_parameter"] rec pp :
-    type a. Format.formatter -> a t -> unit =
+let rec pp : type a. Format.formatter -> a t -> unit =
  fun ppf {dir; _} ->
   match dir with
   | Empty -> Format.fprintf ppf "Empty"
@@ -72,8 +71,7 @@ let[@coq_struct "function_parameter"] rec pp :
       let name = Format.asprintf "<%s>" (RPC_arg.descr arg).name in
       pp_item ppf (name, subdir)
 
-and[@coq_mutual_as_notation] pp_item :
-    type a. Format.formatter -> string * a t -> unit =
+and pp_item : type a. Format.formatter -> string * a t -> unit =
  fun ppf (name, desc) -> Format.fprintf ppf "@[<hv 2>%s@ %a@]" name pp desc
 
 let pp_rev_path ppf path =
diff --git a/src/proto_alpha/lib_protocol/tez_repr.ml b/src/proto_alpha/lib_protocol/tez_repr.ml
index 99bbe0b87d09bc2aed1e188d473e6e1d3f8d838a..c8a8aa98b69973d2736a5ada331359254ab1e4dc 100644
--- a/src/proto_alpha/lib_protocol/tez_repr.ml
+++ b/src/proto_alpha/lib_protocol/tez_repr.ml
@@ -97,7 +97,7 @@ let of_string s =
 
 let pp ppf (Tez_tag amount) =
   let mult_int = 1_000_000L in
-  let[@coq_struct "amount"] rec left ppf amount =
+  let rec left ppf amount =
     let d, r = (Int64.(div amount 1000L), Int64.(rem amount 1000L)) in
     if d > 0L then Format.fprintf ppf "%a%03Ld" left d r
     else Format.fprintf ppf "%Ld" r