From 9faf51a7c79175036f2c849f6d0cefe845131962 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 21 Feb 2025 18:44:45 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#20278. --- apps/coercion/src/rocq_elpi_coercion_hook.mlg | 4 ++-- apps/cs/src/rocq_elpi_cs_hook.mlg | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/apps/coercion/src/rocq_elpi_coercion_hook.mlg b/apps/coercion/src/rocq_elpi_coercion_hook.mlg index 4fa00bf39..e6e7e95e1 100644 --- 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 \ No newline at end of file +END diff --git a/apps/cs/src/rocq_elpi_cs_hook.mlg b/apps/cs/src/rocq_elpi_cs_hook.mlg index 8149683d8..ee4c07823 100644 --- 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 =