diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index dd719e48e4..f4ed6694e5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -282,7 +282,7 @@ let extract_open_proof sigma pf = let visible_rels = map_succeed (fun id -> - try let n = list_index id vl in (n,id) + try let n = proof_variable_index id vl in (n,id) with Not_found -> failwith "caught") (ids_of_named_context (named_context_of_val goal.evar_hyps)) in let sorted_rels = |