Merge pull request #781 from ppedrot/rm-tc-evd-hook

Adapt w.r.t. coq/coq#20278.
LPCIC · Feb 22, 2025 · 19cc599 · 19cc599
2 parents 2560ad0 + 9faf51a
commit 19cc599
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/apps/coercion/src/rocq_elpi_coercion_hook.mlg b/apps/coercion/src/rocq_elpi_coercion_hook.mlg
@@ -26,7 +26,7 @@ let return s g t = Some (s,g,t)
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
   let atts = [] in
   let sigma, expected, retype = build_expected_type env sigma expected in
-  let sigma, goal = Evarutil.new_evar env sigma expected in
+  let sigma, goal = Evarutil.new_evar ~typeclass_candidate:false env sigma expected in
   let goal_evar, _ = EConstr.destEvar sigma goal in
   let query state =
     let loc = Elpi.API.State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
@@ -79,4 +79,4 @@ VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      add_coercion_hook (snd p) }
 
-END
+END
diff --git a/apps/cs/src/rocq_elpi_cs_hook.mlg b/apps/cs/src/rocq_elpi_cs_hook.mlg
@@ -11,7 +11,7 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
 	  let atts = [] in
      let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list args2 Reductionops.Stack.empty) in
      let sigma, (goal_ty, _) = Evarutil.new_type_evar env sigma Evd.UnivRigid in
-	  let sigma, goal = Evarutil.new_evar env sigma goal_ty in
+	  let sigma, goal = Evarutil.new_evar ~typeclass_candidate:false env sigma goal_ty in
 	  let goal_evar, _ = EConstr.destEvar sigma goal in
     let nparams = Structures.Structure.projection_nparams proji in
 	  let query state =