diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /engine/termops.mli | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 709fa361a9..12df61e4c8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -50,16 +50,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> (** {6 Generic iterators on constr} *) val map_constr_with_binders_left_to_right : - Evd.evar_map -> + Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : - Evd.evar_map -> - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr -val map_constr_with_full_binders_user_view : - Evd.evar_map -> + Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr @@ -73,7 +69,7 @@ val map_constr_with_full_binders_user_view : val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val fold_constr_with_full_binders : Evd.evar_map -> +val fold_constr_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b |