Add coercion hook

doc/changelog/13-misc/17794-coercion_hook.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  a hook in the coercion mechanism to enable programming coercions in
+  external metalanguages such as Ltac, Ltac2, Elpi or OCaml plugins
+  (`#17794 <https://github.com/coq/coq/pull/17794>`_,
+  by Pierre Roux).

pretyping/coercion.ml

@@ -622,6 +622,13 @@ let lookup_reversible_path_to_common_point env sigma ~src_expected ~src_inferred
   in
     aux r
 
+type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr ->
+  inferred:types -> expected:types -> (evar_map * constr) option
+let hook = Summary.ref ~name:"coercion_hook"
+  (fun _ _ ~flags _ ~inferred ~expected -> None)
+let get_hook () = !hook
+let set_hook f = hook := f
+
 let add_reverse_coercion env sigma v'_ty v_ty v' v =
   match Coqlib.lib_ref_opt "core.coercion.reverse_coercion" with
   | None -> sigma, v'
@@ -657,7 +664,10 @@ let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty ta
       unify_leq_delay ~flags env sigma v'_ty target_type, v', trace
     with (Evarconv.UnableToUnify _ | Not_found) as exn ->
       let _, info = Exninfo.capture exn in
-      Exninfo.iraise (NoCoercion,info)
+      (* 3 if none of the above works, try hook *)
+      match !hook env sigma ~flags v ~inferred:v_ty ~expected:target_type with
+      | Some (sigma, r) -> (sigma, r, ReplaceCoe r)
+      | None -> Exninfo.iraise (NoCoercion,info)
 
 let default_flags_of env =
   default_flags_of TransparentState.full

pretyping/coercion.mli

@@ -58,6 +58,10 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> resolve_tc:boo
 val inh_pattern_coerce_to :
   ?loc:Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern
 
+type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr ->
+  inferred:types -> expected:types -> (evar_map * constr) option
+val get_hook : unit -> hook
+val set_hook : hook -> unit
 
 type delayed_app_body