diff --git a/src/proto_alpha/lib_plugin/RPC.ml b/src/proto_alpha/lib_plugin/RPC.ml
index de3553f8f64351d0141235c30a83aebba12dfba4..7f26714bb53e344d0c43dea994fd6c5dd4132cdc 100644
--- a/src/proto_alpha/lib_plugin/RPC.ml
+++ b/src/proto_alpha/lib_plugin/RPC.ml
@@ -2300,9 +2300,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/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli
index e340830d818887a0a264618bcea2d8f072a835aa..195a5b0c6de8301976f428f75fc21142740f457a 100644
--- a/src/proto_alpha/lib_protocol/alpha_context.mli
+++ b/src/proto_alpha/lib_protocol/alpha_context.mli
@@ -364,7 +364,6 @@ module Gas : sig
   module Arith :
     Fixed_point_repr.Safe
       with type 'a t = private Saturation_repr.may_saturate Saturation_repr.t
-  [@@coq_plain_module]
 
   (** For maintenance operations or for testing, gas can be
      [Unaccounted]. Otherwise, the computation is [Limited] by the
diff --git a/src/proto_alpha/lib_protocol/apply.ml b/src/proto_alpha/lib_protocol/apply.ml
index 23bdab2df0fc12f56357fbf4b9cce813fe5a7f4b..b2a15b999d708833236c291de52c84ce8f0b60f1 100644
--- a/src/proto_alpha/lib_protocol/apply.ml
+++ b/src/proto_alpha/lib_protocol/apply.ml
@@ -1907,7 +1907,7 @@ let apply_manager_operation :
 type success_or_failure = Success of context | Failure
 
 let apply_internal_operations ctxt ~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)
@@ -2164,14 +2164,7 @@ let apply_manager_contents (type kind) ctxt chain_id
     * kind manager_operation_result
     * packed_internal_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
@@ -2251,7 +2244,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
@@ -2329,7 +2322,7 @@ let rec apply_manager_contents_list_rec :
     (success_or_failure * kind Kind.manager contents_result_list) Lwt.t =
  fun ctxt ~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 chain_id op
       >|= fun (ctxt_result, operation_result, internal_operation_results) ->
@@ -2867,7 +2860,7 @@ let apply_contents_list (type kind) ctxt chain_id (apply_mode : apply_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 9a4bec05c0ec5057c04891a10deb10f1cf87a169..e625c311843b805d573f5c0bb769edbdc1c2b1cf 100644
--- a/src/proto_alpha/lib_protocol/apply_internal_results.ml
+++ b/src/proto_alpha/lib_protocol/apply_internal_results.ml
@@ -214,9 +214,8 @@ module Internal_operation = struct
         inj : 'a -> 'kind internal_operation_contents;
       }
         -> 'kind case
-  [@@coq_force_gadt]
 
-  let[@coq_axiom_with_reason "gadt"] transaction_contract_variant_cases =
+  let transaction_contract_variant_cases =
     union
       [
         case
@@ -320,7 +319,7 @@ module Internal_operation = struct
                 Transaction_to_sc_rollup_result {consumed_gas; inbox_after});
       ]
 
-  let[@coq_axiom_with_reason "gadt"] transaction_case =
+  let transaction_case =
     MCase
       {
         (* This value should be changed with care: maybe receipts are read by
@@ -367,7 +366,7 @@ module Internal_operation = 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
@@ -397,7 +396,7 @@ module Internal_operation = 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
@@ -419,7 +418,7 @@ module Internal_operation = struct
         inj = (fun key -> Delegation key);
       }
 
-  let[@coq_axiom_with_reason "gadt"] event_case =
+  let event_case =
     MCase
       {
         (* This value should be changed with care: maybe receipts are read by
@@ -560,7 +559,7 @@ module Internal_operation_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_operation.transaction_case
       ~encoding:Internal_operation.transaction_contract_variant_cases
@@ -572,7 +571,7 @@ module Internal_operation_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_operation.origination_case
       ~encoding:
@@ -637,8 +636,7 @@ module Internal_operation_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})
 
   let event_case =
@@ -652,8 +650,7 @@ module Internal_operation_result = struct
             Some op
         | _ -> None)
       ~kind:Kind.Event_manager_kind
-      ~proj:(function[@coq_match_with_default]
-        | IEvent_result {consumed_gas} -> consumed_gas)
+      ~proj:(function IEvent_result {consumed_gas} -> consumed_gas)
       ~inj:(fun consumed_gas -> IEvent_result {consumed_gas})
 end
 
diff --git a/src/proto_alpha/lib_protocol/apply_operation_result.ml b/src/proto_alpha/lib_protocol/apply_operation_result.ml
index d82aec0e522a548de9758e16630b58e58b6442d9..d5763a4a8050053dcf67416e5a1734979475af28 100644
--- a/src/proto_alpha/lib_protocol/apply_operation_result.ml
+++ b/src/proto_alpha/lib_protocol/apply_operation_result.ml
@@ -32,7 +32,6 @@ type ('kind, 'manager, 'successful) operation_result =
       'manager * error trace
       -> ('kind, 'manager, 'successful) operation_result
   | Skipped : 'manager -> ('kind, 'manager, 'successful) operation_result
-[@@coq_force_gadt]
 
 let error_encoding =
   def
diff --git a/src/proto_alpha/lib_protocol/apply_operation_result.mli b/src/proto_alpha/lib_protocol/apply_operation_result.mli
index 11704df359d9fcefebbf45e99ed1a82aef6dc0df..e48842e3ca719d29d5cf37a36b197fcf6198faaa 100644
--- a/src/proto_alpha/lib_protocol/apply_operation_result.mli
+++ b/src/proto_alpha/lib_protocol/apply_operation_result.mli
@@ -39,6 +39,5 @@ type ('kind, 'manager, 'successful) operation_result =
       'manager * error trace
       -> ('kind, 'manager, 'successful) operation_result
   | Skipped : 'manager -> ('kind, 'manager, 'successful) operation_result
-[@@coq_force_gadt]
 
 val trace_encoding : error trace Data_encoding.t
diff --git a/src/proto_alpha/lib_protocol/apply_results.ml b/src/proto_alpha/lib_protocol/apply_results.ml
index e3edc5bbe3bb96e026d2b771dc291819f38d4dcd..95e44389ddbde1ea28f6951968e062abdd0272cb 100644
--- a/src/proto_alpha/lib_protocol/apply_results.ml
+++ b/src/proto_alpha/lib_protocol/apply_results.ml
@@ -280,7 +280,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:
@@ -293,7 +293,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
@@ -397,7 +397,7 @@ module Manager_result = struct
                 Transaction_to_sc_rollup_result {consumed_gas; inbox_after});
       ]
 
-  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
@@ -408,7 +408,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:
@@ -461,7 +461,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
@@ -495,8 +495,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 =
@@ -533,7 +532,7 @@ module Manager_result = struct
       ~inj:(fun (balance_updates, consumed_gas) ->
         Increase_paid_storage_result {balance_updates; 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:
@@ -555,7 +554,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:
@@ -577,7 +576,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:
@@ -595,7 +594,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:
@@ -614,7 +613,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
@@ -638,7 +637,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
@@ -662,7 +661,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:
@@ -681,7 +680,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
@@ -705,7 +704,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:
@@ -726,7 +725,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
@@ -741,7 +740,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:
@@ -901,7 +900,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:
@@ -920,7 +919,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
@@ -1024,7 +1023,7 @@ type packed_contents_and_result =
       'kind Operation.contents * 'kind contents_result
       -> packed_contents_and_result
 
-type ('a, 'b) eq = Eq : ('a, 'a) eq [@@coq_force_gadt]
+type ('a, 'b) eq = Eq : ('a, 'a) eq
 
 let equal_manager_kind :
     type a b. a Kind.manager -> b Kind.manager -> (a, b) eq option =
@@ -1146,7 +1145,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;
@@ -1174,7 +1173,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;
@@ -1199,7 +1198,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;
@@ -1217,7 +1216,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;
@@ -1236,7 +1235,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;
@@ -1254,7 +1253,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;
@@ -1274,7 +1273,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;
@@ -1295,7 +1294,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;
@@ -1314,7 +1313,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;
@@ -1333,7 +1332,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;
@@ -1349,7 +1348,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;
@@ -1365,7 +1364,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 =
@@ -1448,7 +1447,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
@@ -1458,7 +1457,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
@@ -1468,7 +1467,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
@@ -1478,7 +1477,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
@@ -1488,7 +1487,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
@@ -1500,7 +1499,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
@@ -1511,7 +1510,7 @@ module Encoding = struct
             Some (op, res)
         | _ -> None)
 
-  let[@coq_axiom_with_reason "gadt"] increase_paid_storage_case =
+  let increase_paid_storage_case =
     make_manager_case
       Operation.Encoding.increase_paid_storage_case
       Manager_result.increase_paid_storage_case
@@ -1522,7 +1521,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
@@ -1533,7 +1532,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
@@ -1544,7 +1543,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
@@ -1555,7 +1554,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
@@ -1566,7 +1565,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
@@ -1578,7 +1577,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
@@ -1590,7 +1589,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
@@ -1601,7 +1600,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
@@ -1613,7 +1612,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
@@ -1624,7 +1623,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
@@ -1636,7 +1635,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
@@ -1647,7 +1646,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
@@ -1658,7 +1657,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
@@ -1669,7 +1668,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
@@ -1680,7 +1679,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
@@ -1691,7 +1690,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
@@ -1702,7 +1701,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
@@ -1714,7 +1713,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
@@ -1725,7 +1724,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
@@ -2702,7 +2701,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 e1073e1253d94346012a10dbd1fe14a8c360fa0f..eff662ff50bc4abdc390c95d11f56b76e1d9a4b0 100644
--- a/src/proto_alpha/lib_protocol/contract_repr.ml
+++ b/src/proto_alpha/lib_protocol/contract_repr.ml
@@ -182,7 +182,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/contract_storage.ml b/src/proto_alpha/lib_protocol/contract_storage.ml
index 6a8ea9cf2c7aa10c67fed93c715b1d0d12728c86..4e17ed75ccb66d1196853e61327d6246276f9c05 100644
--- a/src/proto_alpha/lib_protocol/contract_storage.ml
+++ b/src/proto_alpha/lib_protocol/contract_storage.ml
@@ -396,7 +396,6 @@ module Legacy_big_map_diff = struct
       []
       diffs
     |> List.rev |> List.flatten
-    [@@coq_axiom_with_reason "gadt"]
 end
 
 let update_script_lazy_storage c = function
diff --git a/src/proto_alpha/lib_protocol/coq-of-ocaml/README.md b/src/proto_alpha/lib_protocol/coq-of-ocaml/README.md
deleted file mode 100644
index dc8bbda5de5eb6bd2caec1528fd085459d89328c..0000000000000000000000000000000000000000
--- a/src/proto_alpha/lib_protocol/coq-of-ocaml/README.md
+++ /dev/null
@@ -1,11 +0,0 @@
-# coq-of-ocaml
-
-In this folder we put the files relevant to the compilation of the protocol to
-Coq using [coq-of-ocaml](https://clarus.github.io/coq-of-ocaml/). The code of
-the protocol is annotated with `[@coq_...]` OCaml attributes. These attributes
-are here to help the compilation to Coq. We document them on:
-https://clarus.github.io/coq-of-ocaml/docs/attributes
-
-* `config.json` This file describes the configuration parameters for
-  coq-of-ocaml in the CI. For more information, see the
-  [documentation](https://clarus.github.io/coq-of-ocaml/docs/configuration).
diff --git a/src/proto_alpha/lib_protocol/coq-of-ocaml/config.json b/src/proto_alpha/lib_protocol/coq-of-ocaml/config.json
deleted file mode 100644
index 2084143d4b693831336fadfb9725c087f0471a5f..0000000000000000000000000000000000000000
--- a/src/proto_alpha/lib_protocol/coq-of-ocaml/config.json
+++ /dev/null
@@ -1,258 +0,0 @@
-{
-  "alias_barrier_modules": [
-    "Tezos_protocol_environment_alpha__Environment"
-  ],
-  "constant_warning": false,
-  "constructor_map": [
-    ["public_key_hash", "Ed25519", "Ed25519Hash"],
-    ["public_key_hash", "P256", "P256Hash"],
-    ["public_key_hash", "Secp256k1", "Secp256k1Hash"]
-  ],
-  "error_category_blacklist": [
-    "side_effect"
-  ],
-  "error_filename_blacklist": [
-  ],
-  "error_message_blacklist": [
-    "Unbound module Tezos_protocol_alpha_functor",
-    "The placeholders `_` in types are not handled",
-    "No type known for the following variants: `Ge, `Lt, `Eq, `Le, `Gt",
-    "No type known for the following variants: `Eq, `Ge, `Gt, `Le, `Lt",
-    "No type known for the following variants: `Eq",
-    "Constructor of the variant `Eq unknown",
-    "No type known for the following variants: `Tree, `Value",
-    "Constructor of the variant `Tree unknown",
-    "Constructor of the variant `Value unknown",
-    "Anonymous definition of signatures is not handled",
-    "A variable name instead of a pattern was expected",
-    "We only support extensible types in patterns at the head",
-    "This kind of signature is not handled",
-    "Tezos_raw_protocol_alpha.Raw_context_intf.T",
-    "No type known for the following variants:",
-    "Constructor of the variant",
-    "Polymorphic variant types are defined as standard algebraic types",
-    "Mutual type definitions in signatures not handled.",
-    "Did not find a module signature name for the following shape:\n[ max_int; min_int ]",
-    "Unreachable expressions are not supported"
-  ],
-  "escape_value": [
-    "a",
-    "acc",
-    "alloc",
-    "b",
-    "baking_rights_query",
-    "case",
-    "cons",
-    "context",
-    "descr",
-    "diff",
-    "elt",
-    "endorsing_rights_query",
-    "eq",
-    "error",
-    "field",
-    "fixed",
-    "fp",
-    "frozen_balance",
-    "gas_counter_status",
-    "handler",
-    "has_big_map",
-    "has_lazy_storage",
-    "hash",
-    "info",
-    "init",
-    "integral",
-    "internal_gas",
-    "json",
-    "json_schema",
-    "judgement",
-    "key",
-    "kind",
-    "l",
-    "lazy_expr",
-    "level_query",
-    "list_query",
-    "may_saturate",
-    "mul_safe",
-    "namespace",
-    "nonce",
-    "query",
-    "p",
-    "parametric",
-    "r",
-    "raw",
-    "seed",
-    "sequence",
-    "snapshot",
-    "stack",
-    "storage",
-    "storage_error",
-    "t",
-    "tc_context",
-    "toplevel",
-    "trace",
-    "type_logger"
-  ],
-  "first_class_module_path_blacklist": [
-    "Tezos_raw_protocol_alpha",
-    "Tezos_protocol_environment_alpha.Environment",
-    "Tezos_protocol_environment_alpha.Environment.Sapling"
-  ],
-  "first_class_module_signature_blacklist": [
-    "Environment_context.TREE",
-    "Tezos_protocol_environment_alpha__Environment.Map.OrderedType",
-    "Tezos_protocol_environment_alpha__Environment.Set.OrderedType",
-    "Tezos_raw_protocol_alpha__Raw_context.T",
-    "Tezos_raw_protocol_alpha.Alpha_context.Cache.CLIENT",
-    "Tezos_raw_protocol_alpha.Alpha_context.Cache.INTERFACE",
-    "Tezos_sapling__Core_sig.T_encoding"
-  ],
-  "merge_returns": [
-    ["return=", "return?", "return=?"]
-  ],
-  "merge_types": [
-    ["M=", "M?", "M=?"]
-  ],
-  "monadic_lets": [
-    ["Error_monad.op_gtgteq", "let="],
-    ["Error_monad.op_gtgteqquestion", "let=?"],
-    ["Error_monad.op_gtgtquestion", "let?"]
-  ],
-  "monadic_let_returns": [
-    ["Error_monad.op_gtpipeeq", "let=", "return="],
-    ["Error_monad.op_gtpipeeqquestion", "let=?", "return=?"],
-    ["Error_monad.op_gtpipequestion", "let?", "return?"]
-  ],
-  "monadic_returns": [
-    ["Lwt.__return", "return="],
-    ["Error_monad.__return", "return=?"],
-    ["Error_monad.ok", "return?"]
-  ],
-  "monadic_return_lets": [
-    ["Error_monad.op_gtgtquestioneq", "return=", "let=?"]
-  ],
-  "operator_infix": [
-    ["Compare.Int.(Compare.S.op_eq)", "=i"],
-    ["Compare.Int.(Compare.S.op_ltgt)", "<>i"],
-    ["Compare.Int.(Compare.S.op_lteq)", "<=i"],
-    ["Compare.Int.(Compare.S.op_lt)", "<i"],
-    ["Compare.Int.(Compare.S.op_gteq)", ">=i"],
-    ["Compare.Int.(Compare.S.op_gt)", ">i"],
-
-    ["Compare.Int32.(Compare.S.op_eq)", "=i32"],
-    ["Compare.Int32.(Compare.S.op_ltgt)", "<>i32"],
-    ["Compare.Int32.(Compare.S.op_lteq)", "<=i32"],
-    ["Compare.Int32.(Compare.S.op_lt)", "<i32"],
-    ["Compare.Int32.(Compare.S.op_gteq)", ">=i32"],
-    ["Compare.Int32.(Compare.S.op_gt)", ">i32"],
-
-    ["Compare.Int64.(Compare.S.op_eq)", "=i64"],
-    ["Compare.Int64.(Compare.S.op_ltgt)", "<>i64"],
-    ["Compare.Int64.(Compare.S.op_lteq)", "<=i64"],
-    ["Compare.Int64.(Compare.S.op_lt)", "<i64"],
-    ["Compare.Int64.(Compare.S.op_gteq)", ">=i64"],
-    ["Compare.Int64.(Compare.S.op_gt)", ">i64"],
-
-    ["Compare.Z.(Compare.S.op_eq)", "=Z"],
-    ["Compare.Z.(Compare.S.op_ltgt)", "<>Z"],
-    ["Compare.Z.(Compare.S.op_lteq)", "<=Z"],
-    ["Compare.Z.(Compare.S.op_lt)", "<Z"],
-    ["Compare.Z.(Compare.S.op_gteq)", ">=Z"],
-    ["Compare.Z.(Compare.S.op_gt)", ">Z"],
-
-    ["Int32.add", "+i32"],
-    ["Int32.sub", "-i32"],
-    ["Int32.mul", "*i32"],
-    ["Int32.div", "/i32"],
-
-    ["Int64.add", "+i64"],
-    ["Int64.sub", "-i64"],
-    ["Int64.mul", "*i64"],
-    ["Int64.div", "/i64"],
-
-    ["Pervasives.op_andand", "&&"],
-    ["Pervasives.op_pipepipe", "||"],
-
-    ["Pervasives.op_plus", "+i"],
-    ["Pervasives.op_minus", "-i"],
-    ["Pervasives.op_star", "*i"],
-    ["Pervasives.op_div", "/i"],
-
-    ["Z.add", "+Z"],
-    ["Z.sub", "-Z"],
-    ["Z.mul", "*Z"],
-    ["Z.div", "/Z"],
-
-    ["Z_syntax.op_plus", "+Z"],
-    ["Z_syntax.op_star", "*Z"]
-  ],
-  "renaming_rules": [
-    ["Error_monad.tzresult", "M?"],
-    ["Lwt.t", "M="],
-    ["Failure", "Failure"]
-  ],
-  "renaming_type_constructor": [
-    ["Compare.Char.(Compare.S.t)", "ascii"],
-    ["Compare.Int.(Compare.S.t)", "int"],
-    ["Compare.Int32.(Compare.S.t)", "int32"],
-    ["Compare.Int64.(Compare.S.t)", "int64"],
-    ["Compare.String.(Compare.S.t)", "string"],
-    ["Compare.Z.(Compare.S.t)", "Z.t"]
-  ],
-  "require": [
-    ["Tezos_raw_protocol_alpha", "TezosOfOCaml.Proto_alpha"]
-  ],
-  "require_import": [
-    ["Tezos_protocol_environment_alpha", "TezosOfOCaml.Proto_alpha"]
-  ],
-  "require_long_ident": [
-    ["Storage_description", "TezosOfOCaml.Proto_alpha"]
-  ],
-  "require_mli": [
-  ],
-  "variant_constructors": [
-    ["Dir", "Context.Dir"],
-    ["Key", "Context.Key"],
-    ["Uint16", "Data_encoding.Uint16"],
-    ["Uint8", "Data_encoding.Uint8"],
-    ["Hex", "Hex.Hex"],
-    ["Branch", "Error_monad.Branch"],
-    ["Permanent", "Error_monad.Permanent"],
-    ["Temporary", "Error_monad.Temporary"]
-  ],
-  "variant_types": [
-    ["Dir", "Context.key_or_dir"],
-    ["Key", "Context.key_or_dir"]
-  ],
-  "without_guard_checking": [
-    "apply.ml",
-    "apply_results.ml",
-    "baking.ml",
-    "contract_repr.ml",
-    "delegate_services.ml",
-    "fixed_point_repr.ml",
-    "helpers_services.ml",
-    "lazy_storage_kind.ml",
-    "legacy_script_support_repr.ml",
-    "level_storage.ml",
-    "michelson_v1_gas.ml",
-    "michelson_v1_primitives.ml",
-    "misc.ml",
-    "operation_repr.ml",
-    "raw_context.ml",
-    "roll_storage.ml",
-    "sapling_storage.ml",
-    "script_interpreter.ml",
-    "script_ir_annot.ml",
-    "script_ir_translator.ml",
-    "script_repr.ml",
-    "seed_repr.ml",
-    "storage_description.ml",
-    "storage_functors.ml",
-    "tez_repr.ml"
-  ],
-  "without_positivity_checking": [
-    "misc.ml",
-    "storage_description.ml"
-  ]
-}
diff --git a/src/proto_alpha/lib_protocol/fixed_point_repr.ml b/src/proto_alpha/lib_protocol/fixed_point_repr.ml
index 531fd045f4537cc658ad344d4bfeade036ac281b..079c864431095b6574c762613e020943944e6d9f 100644
--- a/src/proto_alpha/lib_protocol/fixed_point_repr.ml
+++ b/src/proto_alpha/lib_protocol/fixed_point_repr.ml
@@ -28,7 +28,7 @@ type fp_tag (* Tag for fixed point computations *)
 type integral_tag (* Tag for integral computations *)
 
 module type Safe = sig
-  type 'a t [@@coq_phantom]
+  type 'a t
 
   type fp = fp_tag t
 
@@ -86,7 +86,7 @@ module type Safe = sig
 end
 
 module type Full = sig
-  type 'a t [@@coq_phantom]
+  type 'a t
 
   include Safe with type 'a t := 'a t
 
diff --git a/src/proto_alpha/lib_protocol/fixed_point_repr.mli b/src/proto_alpha/lib_protocol/fixed_point_repr.mli
index a9dee73a6f6e5a96d4818845ef5664425a91106f..a5f513fe4dbe471530b8a0a331f287880e675563 100644
--- a/src/proto_alpha/lib_protocol/fixed_point_repr.mli
+++ b/src/proto_alpha/lib_protocol/fixed_point_repr.mli
@@ -39,7 +39,7 @@ type integral_tag (* Tag for integral computations *)
     Such numbers represent standard arithmetic, rounding (converting fp
     flavour to integral one) and comparisons (which can work across flavours). *)
 module type Safe = sig
-  type 'a t [@@coq_phantom]
+  type 'a t
 
   type fp = fp_tag t
 
@@ -97,7 +97,7 @@ module type Safe = sig
 end
 
 module type Full = sig
-  type 'a t [@@coq_phantom]
+  type 'a t
 
   include Safe with type 'a t := 'a t
 
diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.mli b/src/proto_alpha/lib_protocol/gas_limit_repr.mli
index 834836551f282383c13e9e6d69d2c876e377bfb9..dbecfda6fd6ba8bfac509213198043d919899597 100644
--- a/src/proto_alpha/lib_protocol/gas_limit_repr.mli
+++ b/src/proto_alpha/lib_protocol/gas_limit_repr.mli
@@ -42,7 +42,6 @@
 module Arith :
   Fixed_point_repr.Full
     with type 'a t = private Saturation_repr.may_saturate Saturation_repr.t
-[@@coq_plain_module]
 
 type t = Unaccounted | Limited of {remaining : Arith.fp}
 
diff --git a/src/proto_alpha/lib_protocol/global_constants_storage.ml b/src/proto_alpha/lib_protocol/global_constants_storage.ml
index f00b2f3330c512b46578e8d1d399acd0d66d7ee7..be7b9dc62f46ec3f8b1acd54d673b81ba26c1bf1 100644
--- a/src/proto_alpha/lib_protocol/global_constants_storage.ml
+++ b/src/proto_alpha/lib_protocol/global_constants_storage.ml
@@ -56,7 +56,6 @@ let bottom_up_fold_cps initial_accumulator node initial_k f =
                 k accu (node :: nodes)))
   in
   traverse_node initial_accumulator node initial_k
-  [@@coq_axiom_with_reason "local mutually recursive definition not handled"]
 
 module Gas_costs = Global_constants_costs
 module Expr_hash_map = Map.Make (Script_expr_hash)
diff --git a/src/proto_alpha/lib_protocol/lazy_storage_diff.ml b/src/proto_alpha/lib_protocol/lazy_storage_diff.ml
index a6126aabfe946bd65d813dbeb7b278deec114b85..791b3f828448f71a918fbe489b848a6e4e559c6b 100644
--- a/src/proto_alpha/lib_protocol/lazy_storage_diff.ml
+++ b/src/proto_alpha/lib_protocol/lazy_storage_diff.ml
@@ -186,7 +186,6 @@ let get_ops : type i a u. (i, a, u) Lazy_storage_kind.t -> (i, a, u) ops =
   function
   | Big_map -> (module Big_map)
   | Sapling_state -> (module Sapling_state)
-  [@@coq_axiom_with_reason "gadt"]
 
 type ('id, 'alloc) init = Existing | Copy of {src : 'id} | Alloc of 'alloc
 
@@ -371,7 +370,6 @@ let item_encoding =
              | Neq -> None)
            (fun ((), id, diff) -> Item (k, id, diff)))
        Lazy_storage_kind.all
-  [@@coq_axiom_with_reason "gadt"]
 
 let item_in_memory_size
     (Item
@@ -415,7 +413,6 @@ let fresh :
   else
     let (module OPS) = get_ops kind in
     OPS.Next.incr ctxt
- [@@coq_axiom_with_reason "gadt"]
 
 let init ctxt =
   List.fold_left_es
@@ -424,7 +421,6 @@ let init ctxt =
       OPS.Next.init ctxt)
     ctxt
     Lazy_storage_kind.all
-  [@@coq_axiom_with_reason "gadt"]
 
 let cleanup_temporaries ctxt =
   Raw_context.map_temporary_lazy_storage_ids_s ctxt (fun temp_ids ->
@@ -435,4 +431,3 @@ let cleanup_temporaries ctxt =
         ctxt
         Lazy_storage_kind.all
       >|= fun ctxt -> (ctxt, Lazy_storage_kind.Temp_ids.init))
-  [@@coq_axiom_with_reason "gadt"]
diff --git a/src/proto_alpha/lib_protocol/lazy_storage_kind.ml b/src/proto_alpha/lib_protocol/lazy_storage_kind.ml
index 59014e154784174e3b46f706ebe5a5825cff7302..03655e7e956e07fbe7c1f4d902ac5037d296ad24 100644
--- a/src/proto_alpha/lib_protocol/lazy_storage_kind.ml
+++ b/src/proto_alpha/lib_protocol/lazy_storage_kind.ml
@@ -248,7 +248,6 @@ module Temp_ids = struct
         let sapling_state = Sapling_state.Temp_id.next temp_ids.sapling_state in
         ( {temp_ids with sapling_state},
           (temp_ids.sapling_state :> Sapling_state.Id.t) )
-   [@@coq_axiom_with_reason "gadt"]
 
   let fold_s :
       type i a u.
@@ -272,7 +271,6 @@ module Temp_ids = struct
           (module Sapling_state.Temp_id)
           ~last:temp_ids.sapling_state
           (fun acc temp_id -> f acc (temp_id :> i))
-   [@@coq_axiom_with_reason "gadt"]
 end
 
 module IdSet = struct
@@ -288,7 +286,6 @@ module IdSet = struct
     | Big_map, {big_map; _} -> Big_map.IdSet.mem id big_map
     | Sapling_state, {sapling_state; _} ->
         Sapling_state.IdSet.mem id sapling_state
-    [@@coq_axiom_with_reason "gadt"]
 
   let add (type i a u) (kind : (i, a, u) kind) (id : i) set =
     match (kind, set) with
@@ -298,7 +295,6 @@ module IdSet = struct
     | Sapling_state, {sapling_state; _} ->
         let sapling_state = Sapling_state.IdSet.add id sapling_state in
         {set with sapling_state}
-    [@@coq_axiom_with_reason "gadt"]
 
   let diff set1 set2 =
     let big_map = Big_map.IdSet.diff set1.big_map set2.big_map in
@@ -306,7 +302,6 @@ module IdSet = struct
       Sapling_state.IdSet.diff set1.sapling_state set2.sapling_state
     in
     {big_map; sapling_state}
-    [@@coq_axiom_with_reason "gadt"]
 
   let fold (type i a u) (kind : (i, a, u) kind) (f : i -> 'acc -> 'acc) set
       (acc : 'acc) =
@@ -314,12 +309,10 @@ module IdSet = struct
     | Big_map, {big_map; _} -> Big_map.IdSet.fold f big_map acc
     | Sapling_state, {sapling_state; _} ->
         Sapling_state.IdSet.fold f sapling_state acc
-    [@@coq_axiom_with_reason "gadt"]
 
   let fold_all f set acc =
     List.fold_left
       (fun acc (_, Ex_Kind kind) -> fold kind (f.f kind) set acc)
       acc
       all
-    [@@coq_axiom_with_reason "gadt"]
 end
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 6cd9197dc56c7713c86d68b46e0162b04844a197..3ce79a43dad7cf385b02568247862d1237aa08f9 100644
--- a/src/proto_alpha/lib_protocol/main.ml
+++ b/src/proto_alpha/lib_protocol/main.ml
@@ -719,7 +719,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_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
index a8e6ae52f419ce76f3935aba7c9cfa981e54ad66..4111d92bb21dc68ddb7d20347ef44302d1c45153 100644
--- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
+++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml
@@ -1441,7 +1441,6 @@ module Cost_of = struct
         | Return -> cost
       in
       compare ty x y Gas.free Return
-     [@@coq_axiom_with_reason "non top-level mutually recursive function"]
 
     let set_mem (type a) (elt : a) (set : a Script_typed_ir.set) =
       let open S_syntax in
diff --git a/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml b/src/proto_alpha/lib_protocol/michelson_v1_primitives.ml
index abbad29046c1dae6433d9fa3e6f53aa9006f2fcc..44c0bf47d21b8734685b631e725f45521bd99c22 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] <> '_')
@@ -566,8 +564,6 @@ let prims_of_strings expr =
     | Seq (loc, args) -> List.map_e convert args >|? fun args -> Seq (loc, args)
   in
   convert (root expr) >|? fun expr -> strip_locations expr
-  [@@coq_axiom_with_reason
-    "implicit type conversion for expr in the constant cases"]
 
 let strings_of_prims expr =
   let rec convert = function
@@ -581,8 +577,6 @@ let strings_of_prims expr =
         Seq (loc, args)
   in
   strip_locations (convert (root expr))
-  [@@coq_axiom_with_reason
-    "implicit type conversion for expr in the constant cases"]
 
 let prim_encoding =
   let open Data_encoding in
diff --git a/src/proto_alpha/lib_protocol/misc.ml b/src/proto_alpha/lib_protocol/misc.ml
index bd350a5ef85b2a35d204d68f06094db9686e565d..817c53730049be9c303bc04c17e3c5c643962ade 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)
 
@@ -63,7 +63,6 @@ let split delim ?(limit = max_int) path =
     else do_component acc limit i (j + 1)
   in
   if Compare.Int.(limit > 0) then do_slashes [] limit 0 else [path]
-  [@@coq_axiom_with_reason "non-top-level mutual recursion"]
 
 let pp_print_paragraph ppf description =
   Format.fprintf
diff --git a/src/proto_alpha/lib_protocol/operation_repr.ml b/src/proto_alpha/lib_protocol/operation_repr.ml
index a402132cf700545537f8c6d406268a2b2868219f..7800df44295d1600d33d1bf73aeee9e2f6fc1f1a 100644
--- a/src/proto_alpha/lib_protocol/operation_repr.ml
+++ b/src/proto_alpha/lib_protocol/operation_repr.ml
@@ -612,9 +612,8 @@ module Encoding = struct
           inj : 'a -> 'kind manager_operation;
         }
           -> 'kind case
-    [@@coq_force_gadt]
 
-    let[@coq_axiom_with_reason "gadt"] reveal_case =
+    let reveal_case =
       MCase
         {
           tag = 0;
@@ -625,7 +624,7 @@ module Encoding = struct
           inj = (fun pkh -> Reveal pkh);
         }
 
-    let[@coq_axiom_with_reason "gadt"] transaction_case =
+    let transaction_case =
       MCase
         {
           tag = 1;
@@ -662,7 +661,7 @@ module Encoding = struct
               Transaction {amount; destination; parameters; entrypoint});
         }
 
-    let[@coq_axiom_with_reason "gadt"] origination_case =
+    let origination_case =
       MCase
         {
           tag = 2;
@@ -683,7 +682,7 @@ module Encoding = struct
               Origination {credit; delegate; script});
         }
 
-    let[@coq_axiom_with_reason "gadt"] delegation_case =
+    let delegation_case =
       MCase
         {
           tag = 3;
@@ -695,7 +694,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;
@@ -708,7 +707,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;
@@ -721,7 +720,7 @@ module Encoding = struct
           inj = (fun key -> Set_deposits_limit key);
         }
 
-    let[@coq_axiom_with_reason "gadt"] increase_paid_storage_case =
+    let increase_paid_storage_case =
       MCase
         {
           tag = 9;
@@ -742,7 +741,7 @@ module Encoding = struct
               Increase_paid_storage {amount_in_bytes; destination});
         }
 
-    let[@coq_axiom_with_reason "gadt"] tx_rollup_origination_case =
+    let tx_rollup_origination_case =
       MCase
         {
           tag = tx_rollup_operation_origination_tag;
@@ -761,7 +760,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;
@@ -783,7 +782,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;
@@ -803,7 +802,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;
@@ -816,7 +815,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;
@@ -831,7 +830,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;
@@ -846,7 +845,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;
@@ -925,7 +924,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;
@@ -981,7 +980,7 @@ module Encoding = struct
                 });
         }
 
-    let[@coq_axiom_with_reason "gadt"] transfer_ticket_case =
+    let transfer_ticket_case =
       MCase
         {
           tag = transfer_ticket_tag;
@@ -1008,7 +1007,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;
@@ -1033,7 +1032,7 @@ module Encoding = struct
                 {kind; boot_sector; origination_proof; 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;
@@ -1046,7 +1045,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;
@@ -1066,7 +1065,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;
@@ -1085,7 +1084,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;
@@ -1104,7 +1103,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;
@@ -1128,7 +1127,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;
@@ -1146,7 +1145,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;
@@ -1173,7 +1172,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;
@@ -1186,7 +1185,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;
@@ -1274,7 +1273,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,
@@ -1284,7 +1283,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
@@ -1321,15 +1320,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;
@@ -1345,7 +1343,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;
@@ -1357,7 +1355,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
       {
@@ -1375,8 +1373,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;
@@ -1393,7 +1390,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;
@@ -1409,7 +1406,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;
@@ -1428,7 +1425,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;
@@ -1448,7 +1445,7 @@ module Encoding = struct
             Proposals {source; period; proposals});
       }
 
-  let[@coq_axiom_with_reason "gadt"] ballot_case =
+  let ballot_case =
     Case
       {
         tag = 6;
@@ -1477,8 +1474,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);
       }
 
@@ -1490,8 +1486,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)
@@ -1500,7 +1495,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
       {
@@ -1860,7 +1855,7 @@ let hash_packed (o : packed_operation) =
   in
   Operation.hash {shell = o.shell; proto}
 
-type ('a, 'b) eq = Eq : ('a, 'a) eq [@@coq_force_gadt]
+type ('a, 'b) eq = Eq : ('a, 'a) eq
 
 let equal_manager_operation_kind :
     type a b. a manager_operation -> b manager_operation -> (a, b) eq option =
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_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml
index d570ef9bda7669507e559eabf611f893e5fe3509..2156d26610b5e4b4e6349765cb882bbf6bb48875 100644
--- a/src/proto_alpha/lib_protocol/script_comparable.ml
+++ b/src/proto_alpha/lib_protocol/script_comparable.ml
@@ -91,4 +91,3 @@ let compare_comparable : type a. a comparable_ty -> a -> a -> int =
         if Compare.Int.(ret > 0) then 1 else -1
   in
   fun t -> compare_comparable t Compare_comparable_return
-  [@@coq_axiom_with_reason "non top-level mutually recursive function"]
diff --git a/src/proto_alpha/lib_protocol/script_int.mli b/src/proto_alpha/lib_protocol/script_int.mli
index 1dbb5425330dc06fd588367ba34a07daa5005458..449192a3cc59a24c4e30d7fdff2256af079dcf08 100644
--- a/src/proto_alpha/lib_protocol/script_int.mli
+++ b/src/proto_alpha/lib_protocol/script_int.mli
@@ -30,7 +30,7 @@
 
     This is internally a [Z.t].
     This module mostly adds signedness preservation guarantees. *)
-type 't repr [@@coq_phantom]
+type 't repr
 
 (** [num] is made algebraic in order to distinguish it from the other type
     parameters of [Script_typed_ir.ty]. *)
diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
index ff12b7e053ffca060f7dd0d35c52ed5d79637c9f..d88d017df3d4af2092ee74f2d2bdef407d4ea23e 100644
--- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
+++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml
@@ -354,7 +354,6 @@ let cost_of_instr : type a s r f. (a, s, r, f) kinstr -> a -> s -> Gas.cost =
   | IEmit _ -> Interp_costs.emit
   | ILog _ -> Gas.free
  [@@ocaml.inline always]
- [@@coq_axiom_with_reason "unreachable expression `.` not handled"]
 
 let cost_of_control : type a s r f. (a, s, r, f) continuation -> Gas.cost =
  fun ks ->
diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml
index 60392a0046fb0b335a6db30dfcc7b19be50e762e..08569a251d5b04e9cfa8d70d006b80e862c25ec9 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 ->
@@ -524,7 +524,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 ->
@@ -860,7 +860,6 @@ let rec ty_eq :
     | Chest_key_t, _ -> not_equal ()
   in
   help ty1 ty2
- [@@coq_axiom_with_reason "non-top-level mutual recursion"]
 
 (* Same as ty_eq but for stacks.
    A single error monad is used here because there is no need to
@@ -936,7 +935,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))
@@ -968,7 +967,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 ->
@@ -1308,8 +1307,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 ->
@@ -1332,7 +1330,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 ->
@@ -1350,8 +1348,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 ->
@@ -1368,8 +1365,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] ->
@@ -1386,8 +1382,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
@@ -2304,7 +2299,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 ->
@@ -2827,7 +2822,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 ->
@@ -2870,7 +2865,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 ->
@@ -4867,7 +4862,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 ->
@@ -4899,7 +4894,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 ->
@@ -5144,7 +5139,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 ->
@@ -5284,13 +5279,12 @@ let list_entrypoints_uncarbonated (type full fullc) (full : (full, fullc) ty)
         (Entrypoint.Map.singleton name (Ex_ty full, original_type_expr), true)
   in
   fold_tree full entrypoints.root [] reachable ([], init)
-  [@@coq_axiom_with_reason "unsupported syntax"]
 
 (* ---- Unparsing (Typed IR -> Untyped expressions) --------------------------*)
 
 (* -- 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 ->
@@ -5494,7 +5488,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 =
@@ -5813,8 +5807,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 ->
@@ -5925,7 +5918,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 ->
@@ -5984,7 +5977,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
@@ -5994,8 +5987,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
@@ -6072,7 +6065,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 a730986fdd39bc167d03404f901861ccfbcf4801..0313ad63c53f03058c4bc30fb426d7edfa5d86a8 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
     | [] -> (
@@ -314,7 +314,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
@@ -332,8 +332,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/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml
index e0371d154e5fe98d03cb033144792250d7e60f2a..70b8a85d51ef093300733edf54a56877f1d6a127 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml
@@ -1108,7 +1108,6 @@ and ('arg, 'ret) lambda =
   | Lam :
       ('arg, end_of_stack, 'ret, end_of_stack) kdescr * Script.node
       -> ('arg, 'ret) lambda
-[@@coq_force_gadt]
 
 and 'arg typed_destination =
   | Typed_implicit : public_key_hash -> unit typed_destination
@@ -1332,7 +1331,6 @@ and ('value, 'before, 'after) comb_set_gadt_witness =
   | Comb_set_plus_two :
       ('value, 'before, 'after) comb_set_gadt_witness
       -> ('value, 'a * 'before, 'a * 'after) comb_set_gadt_witness
-[@@coq_force_gadt]
 
 and (_, _, _, _) dup_n_gadt_witness =
   | Dup_n_zero : ('a, _, _, 'a) dup_n_gadt_witness
@@ -2151,7 +2149,6 @@ let value_traverse (type t tc) (ty : (t, tc) ty) (x : t) init f =
                 (on_bindings [@ocaml.tailcall]) accu kty ty' continue xs))
   in
   aux init ty x (fun accu -> accu)
-  [@@coq_axiom_with_reason "local mutually recursive definition not handled"]
 
 let stack_top_ty : type a b s. (a, b * s) stack_ty -> a ty_ex_c = function
   | Item_t (ty, _) -> Ty_ex_c ty
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli
index 2899f5ce523d0c331bcf0fac9b0dcbb4fa3a5921..df36a40273641e92042babb380b8156a82444d43 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir.mli
+++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli
@@ -1109,7 +1109,6 @@ and ('arg, 'ret) lambda =
   | Lam :
       ('arg, end_of_stack, 'ret, end_of_stack) kdescr * Script.node
       -> ('arg, 'ret) lambda
-[@@coq_force_gadt]
 
 and 'arg typed_destination =
   | Typed_implicit : public_key_hash -> unit typed_destination
@@ -1453,7 +1452,6 @@ and ('value, 'before, 'after) comb_set_gadt_witness =
   | Comb_set_plus_two :
       ('value, 'before, 'after) comb_set_gadt_witness
       -> ('value, 'a * 'before, 'a * 'after) comb_set_gadt_witness
-[@@coq_force_gadt]
 
 (*
 
diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
index 10df0d4193ffbff44830fd3fece66cb1bfa1cddf..b7d7813edf31dc9ed6f19cdc4f10dbe0444b04e7 100644
--- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
+++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml
@@ -298,7 +298,6 @@ let rec value_size :
     | Chest_t -> ret_succ_adding accu (chest_size x)
   in
   value_traverse ty x accu {apply}
- [@@coq_axiom_with_reason "unreachable expressions '.' not handled for now"]
 
 and big_map_size :
     type a b bc.
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..9b3eb082492f88d7e9a80a3a9da616ea22c1e48a 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 =
@@ -133,7 +131,6 @@ let rec unpack : type a b c. (a, b, c) args -> c -> a * b = function
         let c, d = unpack_r x in
         let b, a = unpack_l c in
         (b, (a, d))
-  [@@coq_axiom_with_reason "gadt"]
 
 let rec pack : type a b c. (a, b, c) args -> a -> b -> c = function
   | One _ -> fun b a -> (b, a)
@@ -143,7 +140,6 @@ let rec pack : type a b c. (a, b, c) args -> a -> b -> c = function
       fun b (a, d) ->
         let c = pack_l b a in
         pack_r c d
-  [@@coq_axiom_with_reason "gadt"]
 
 let rec compare : type a b c. (a, b, c) args -> b -> b -> int = function
   | One {compare; _} -> compare
@@ -152,7 +148,6 @@ let rec compare : type a b c. (a, b, c) args -> b -> b -> int = function
       let compare_r = compare r in
       fun (a1, b1) (a2, b2) ->
         match compare_l a1 a2 with 0 -> compare_r b1 b2 | x -> x)
-  [@@coq_axiom_with_reason "gadt"]
 
 let destutter equal l =
   match l with
@@ -216,7 +211,6 @@ let rec register_indexed_subcontext :
                 (RPC_arg.descr arg).name
                 (RPC_arg.descr inner_arg).name
           | Some RPC_arg.Eq -> subdir))
- [@@coq_axiom_with_reason "gadt"]
 
 let register_value :
     type a b.
@@ -277,7 +271,6 @@ let rec combine_object = function
               handler.get k i >>=? fun v1 ->
               handlers.get k i >|=? fun v2 -> (v1, v2));
         }
-  [@@coq_axiom_with_reason "gadt"]
 
 type query = {depth : int}
 
@@ -385,4 +378,3 @@ let build_directory : type key. key t -> key RPC_directory.t =
   in
   ignore (build_handler dir RPC_path.open_root : key opt_handler) ;
   !rpc_dir
- [@@coq_axiom_with_reason "gadt"]
diff --git a/src/proto_alpha/lib_protocol/storage_functors.ml b/src/proto_alpha/lib_protocol/storage_functors.ml
index 4170b7bb2f5548dd27c8897e7b60ba9fee3fee38..c1d958612b36cb41b5805986b8b28cb021adeb2c 100644
--- a/src/proto_alpha/lib_protocol/storage_functors.ml
+++ b/src/proto_alpha/lib_protocol/storage_functors.ml
@@ -194,7 +194,6 @@ struct
       ~get:find
       (register_named_subcontext description N.name)
       V.encoding
-    [@@coq_axiom_with_reason "stack overflow in Coq"]
 end
 
 module type INDEX = sig
@@ -267,7 +266,6 @@ module Make_data_set_storage (C : Raw_context.T) (I : INDEX) :
          C.description
          I.args)
       Data_encoding.bool
-    [@@coq_axiom_with_reason "stack overflow in Coq"]
 end
 
 module Make_indexed_data_storage (C : Raw_context.T) (I : INDEX) (V : VALUE) :
@@ -351,7 +349,6 @@ struct
          C.description
          I.args)
       V.encoding
-    [@@coq_axiom_with_reason "stack overflow in Coq"]
 end
 
 (* Internal-use-only version of {!Make_indexed_carbonated_data_storage} to
@@ -541,7 +538,6 @@ module Make_indexed_carbonated_data_storage_INTERNAL
          C.description
          I.args)
       V.encoding
-    [@@coq_axiom_with_reason "stack overflow in Coq"]
 end
 
 module Make_indexed_carbonated_data_storage : functor
@@ -879,7 +875,6 @@ module Make_indexed_subcontext (C : Raw_context.T) (I : INDEX) :
           mem c k >>= function true -> return_some true | false -> return_none)
         (register_named_subcontext description N.name)
         Data_encoding.bool
-      [@@coq_axiom_with_reason "stack overflow in Coq"]
   end
 
   module Make_map (N : NAME) (V : VALUE) :
@@ -972,7 +967,6 @@ module Make_indexed_subcontext (C : Raw_context.T) (I : INDEX) :
           find c k)
         (register_named_subcontext Raw_context.description N.name)
         V.encoding
-      [@@coq_axiom_with_reason "stack overflow in Coq"]
   end
 
   module Make_carbonated_map (N : NAME) (V : VALUE) :
@@ -1088,7 +1082,6 @@ module Make_indexed_subcontext (C : Raw_context.T) (I : INDEX) :
           find c k >|=? fun (_, v) -> v)
         (register_named_subcontext Raw_context.description N.name)
         V.encoding
-      [@@coq_axiom_with_reason "stack overflow in Coq"]
   end
 end
 
diff --git a/src/proto_alpha/lib_protocol/storage_sigs.ml b/src/proto_alpha/lib_protocol/storage_sigs.ml
index 7871fc33b00b66a587a79df8b78611283b59ed20..f1db042a94f136b114a99e1d1ca24fa00173ea1f 100644
--- a/src/proto_alpha/lib_protocol/storage_sigs.ml
+++ b/src/proto_alpha/lib_protocol/storage_sigs.ml
@@ -76,7 +76,6 @@ module type Single_data_storage = sig
       the bucket does not exists *)
   val remove : context -> Raw_context.t Lwt.t
 end
-[@@coq_precise_signature]
 
 (** Restricted version of {!Indexed_data_storage} w/o iterators. *)
 module type Non_iterable_indexed_data_storage = sig
@@ -130,7 +129,6 @@ module type Non_iterable_indexed_data_storage = sig
       bucket does not exists. *)
   val remove : context -> key -> Raw_context.t Lwt.t
 end
-[@@coq_precise_signature]
 
 (** Variant of {!Non_iterable_indexed_data_storage} with gas accounting. *)
 module type Non_iterable_indexed_carbonated_data_storage = sig
@@ -212,7 +210,6 @@ module type Non_iterable_indexed_carbonated_data_storage = sig
       indicating if a value was already associated to this key. *)
   val remove : context -> key -> (Raw_context.t * int * bool) tzresult Lwt.t
 end
-[@@coq_precise_signature]
 
 module type Non_iterable_indexed_carbonated_data_storage_with_values = sig
   include Non_iterable_indexed_carbonated_data_storage
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
diff --git a/src/proto_alpha/lib_protocol/voting_services.ml b/src/proto_alpha/lib_protocol/voting_services.ml
index 2422274c5d52b8c24ef4a1a85a2ea34fe8d16db1..b005d4d47a9c27e09eb13153cdacaca65f3bc134 100644
--- a/src/proto_alpha/lib_protocol/voting_services.ml
+++ b/src/proto_alpha/lib_protocol/voting_services.ml
@@ -121,9 +121,6 @@ let register () =
       Vote.find_current_proposal ctxt) ;
   register0 ~chunked:false S.total_voting_power (fun ctxt () () ->
       Vote.get_total_voting_power_free ctxt)
-  [@@coq_axiom_with_reason
-    "disabled because we would need to re-create the error e in order to have \
-     different polymorphic variables"]
 
 let ballots ctxt block = RPC_context.make_call0 S.ballots ctxt block () ()