Don't make too many coercions reversible by default

The doc reads

> By default coercions are not reversible
> except for Record fields specified using :>.

The previous code was making way too many coercion reversible by
default. The new behavior should be closer from the spec in the doc.

doc/changelog/08-vernac-commands-and-options/18705-fix_reversible_coercion.rst

@@ -0,0 +1,11 @@
+- **Changed:**
+  the default reversibility status of most coercions.
+  The refman states that
+
+     By default coercions are not reversible
+     except for Record fields specified using ``:>``.
+
+  The previous code was making way too many coercion reversible by default.
+  The new behavior should be closer from the spec in the doc
+  (`#18705 <https://github.com/coq/coq/pull/18705>`_,
+  by Pierre Roux).

test-suite/output/relaxed_ambiguous_paths.out

@@ -48,18 +48,18 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_A] : D >-> A
-[D_B] : D >-> B (reversible)
-[D_C] : D >-> C (reversible)
-[A'_A] : A' >-> A (reversible)
+[D_B] : D >-> B
+[D_C] : D >-> C
+[A'_A] : A' >-> A
 [reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [B_A'; A'_A] : B >-> A
 [B_A'] : B >-> A'
 [C_A'; A'_A] : C >-> A
 [C_A'] : C >-> A'
 [D_A] : D >-> A
 [D_B; B_A'] : D >-> A'
-[D_B] : D >-> B (reversible)
-[D_C] : D >-> C (reversible)
+[D_B] : D >-> B
+[D_C] : D >-> C
 File "./output/relaxed_ambiguous_paths.v", line 147, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
@@ -72,17 +72,17 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
 [C_A'] : C >-> A'
 [D_A] : D >-> A
 [D_B; B_A'] : D >-> A'
-[D_B] : D >-> B (reversible)
-[D_C] : D >-> C (reversible)
+[D_B] : D >-> B
+[D_C] : D >-> C
 File "./output/relaxed_ambiguous_paths.v", line 156, characters 0-47:
 Warning:
-New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT (reversible) is not definitionally an identity function.
+New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
 [ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 157, characters 0-64:
 Warning:
-New coercion path [unwrap_list; wrap_list] : LIST >-> LIST (reversible) is not definitionally an identity function.
+New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
 [ambiguous-paths,coercions,default]
 File "./output/relaxed_ambiguous_paths.v", line 158, characters 0-51:
 Warning:
-New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE (reversible) is not definitionally an identity function.
+New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
 [ambiguous-paths,coercions,default]

vernac/comAssumption.ml

@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ univs imps impl name =
   let () =
     if is_coe = Vernacexpr.AddCoercion then
       ComCoercion.try_add_new_coercion
-        r ~local:true ~reversible:true in
+        r ~local:true ~reversible:false in
   (r, UVars.Instance.empty)
 
 let instance_of_univ_entry = function
@@ -59,7 +59,7 @@ let declare_axiom is_coe ~local ~kind ?user_warns typ (univs, ubinders) imps nl
   let () =
     if is_coe = Vernacexpr.AddCoercion then
       ComCoercion.try_add_new_coercion
-        gr ~local ~reversible:true in
+        gr ~local ~reversible:false in
   let inst = instance_of_univ_entry univs in
   (gr,inst)
 

vernac/record.ml

@@ -842,7 +842,7 @@ let declare_structure { Record_decl.mie; primitive_proj; impls; globnames; globa
     let cstr = (rsp, 1) in
     let projections = declare_projections rsp (projunivs,ubinders) ~kind:projections_kind inhabitant_id proj_flags implfs fields in
     let build = GlobRef.ConstructRef cstr in
-    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~reversible:true in
+    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~reversible:false in
     let struc = Structure.make (Global.env ()) rsp projections in
     let () = declare_structure_entry struc in
     GlobRef.IndRef rsp

vernac/vernacentries.ml

@@ -80,7 +80,7 @@ module DefAttributes = struct
         f
     in
     let using = Option.map Proof_using.using_from_string using in
-    let reversible = Option.default true reversible in
+    let reversible = Option.default false reversible in
     let () = if Option.has_some clearbody && not (Lib.sections_are_opened())
       then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.")
     in