diff --git a/doc/changelog/08-vernac-commands-and-options/18705-fix_reversible_coercion.rst b/doc/changelog/08-vernac-commands-and-options/18705-fix_reversible_coercion.rst new file mode 100644 index 000000000000..2659aa00e35d --- /dev/null +++ b/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 `_, + by Pierre Roux). diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index 711105f1ff39..906a6a6ffc99 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -48,9 +48,9 @@ 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' @@ -58,8 +58,8 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function. [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] diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index b6ef53c1fbf2..7ad1d4fd017a 100644 --- a/vernac/comAssumption.ml +++ b/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) diff --git a/vernac/record.ml b/vernac/record.ml index 14edcc046960..bf80eea67429 100644 --- a/vernac/record.ml +++ b/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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 991afc4a1529..eb55861547b7 100644 --- a/vernac/vernacentries.ml +++ b/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