aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index 24c2c82f2..4becca907 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -65,9 +65,10 @@ val map_constr_with_named_binders :
(Name.t -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
val map_constr_with_binders_left_to_right :
+ Evd.evar_map ->
(Context.Rel.Declaration.t -> 'a -> 'a) ->
- ('a -> constr -> constr) ->
- 'a -> constr -> constr
+ ('a -> EConstr.constr -> EConstr.constr) ->
+ 'a -> EConstr.constr -> EConstr.constr
val map_constr_with_full_binders :
Evd.evar_map ->
(Context.Rel.Declaration.t -> 'a -> 'a) ->