From b3e274d63bb07cbebaf826362b9021bbf6352e3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Tue, 18 Jun 2024 17:08:29 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#19220. --- src/coq_elpi_builtins.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 4340f0b25..1252fd08f 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -426,9 +426,6 @@ let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority = match hint_priority with | Some p -> UserGiven p | None -> - let rec nb_hyp sigma c = match EConstr.kind sigma c with - | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 - | _ -> 0 in let merge_context_set_opt sigma ctx = match ctx with | None -> sigma @@ -443,9 +440,8 @@ let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority = let cty = Reductionops.nf_betaiota env sigma cty in let sigma' = merge_context_set_opt sigma ctx in let ce = Clenv.mk_clenv_from env sigma' (c,cty) in - let miss = Clenv.clenv_missing ce in + let miss, hyps = Clenv.clenv_missing ce in let nmiss = List.length miss in - let hyps = nb_hyp sigma' cty in Computed (hyps + nmiss) (* TODO: this algorithm is quite inefficient since we have not yet the