Adapt w.r.t. rocq-prover/rocq#19220.

Author: ppedrot

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