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