diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 2a0ebf402..6da2f82ab 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -142,10 +142,11 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = + let pop t = Vars.lift (-1) t in if Int.equal n 0 then Some t else match kind_of_term t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop (EConstr.of_constr b)) else None + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (pop b) else None | _ -> None let evar_dependencies evm oev = |