aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 40b3d0d8b..668ae8777 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -797,9 +797,9 @@ let fold_constr_with_binders sigma g f n acc c =
each binder traversal; it is not recursive and the order with which
subterms are processed is not specified *)
-let iter_constr_with_full_binders g f l c =
+let iter_constr_with_full_binders sigma g f l c =
let open RelDecl in
- match kind c with
+ match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> ()
| Cast (c,_, t) -> f l c; f l t