update coercion hook (due to hook call update in coq)

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -11,6 +11,13 @@ open Coq_elpi_vernacular
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
   let loc = API.Ast.Loc.initial "(unknown)" in
   let atts = [] in
+  let (env, sigma, expected, retype) =
+    match expected with
+    | Coercion.Type t -> (env, sigma, t, false)
+    | Coercion.Product -> begin let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
+      let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in
+      (env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Namegen.default_type_ident)), source, target), true) end
+  | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in (env, sigma, t, true) in
   let sigma, goal = Evarutil.new_evar env sigma expected in
   let goal_evar, _ = EConstr.destEvar sigma goal in
   let query ~depth state =
@@ -21,17 +28,17 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
     let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
     state, (loc, qatts), gls
   in
-  match Interp.get_and_compile program with
-  | None -> None
-  | Some (cprogram, _) ->
-    match Interp.run ~static_check:false cprogram (`Fun query) with
-    | API.Execute.Success solution ->
-      let gls = Evar.Set.singleton goal_evar in
-      let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
-      if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None
-    | API.Execute.NoMoreSteps
-    | API.Execute.Failure -> None
-    | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
+  let cprogram, _ = get_and_compile program in
+  match run ~static_check:false cprogram (`Fun query) with
+  | API.Execute.Success solution ->
+     let gls = Evar.Set.singleton goal_evar in
+     let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
+     if Evd.is_defined sigma goal_evar
+     then let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t)
+     else None
+  | API.Execute.NoMoreSteps
+  | API.Execute.Failure -> None
+  | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
 
 let add_coercion_hook =
   let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
@@ -57,4 +64,4 @@ VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      add_coercion_hook (snd p) }
 
-END
+END

apps/coercion/tests/test_coercion.v

@@ -32,3 +32,20 @@ Check natmul R n : ringType_sort R.
 Check n : ringType_sort R.
 
 End TestNatMul.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ V T E {{ Nat.mul lp:V }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ nat -> nat }} ok.
+
+coercion _ V T E {{ { m : nat | m < lp:V } }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ Type }} ok.
+
+}}.
+Elpi Typecheck coercion.
+
+Check 3 2.
+Check forall (x : 3), proj1_sig x < 3.
+