diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 00:07:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /pretyping/glob_ops.mli | |
parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
Diffstat (limited to 'pretyping/glob_ops.mli')
-rw-r--r-- | pretyping/glob_ops.mli | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 124440f5d..c967f4e88 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,8 @@ open Glob_term (** Equalities *) +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t @@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_type_eq : ('a -> 'a -> bool) -> - 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + 'a cast_type -> 'a cast_type -> bool val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool +(** Mapping [cast_type] *) + +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type +val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type + (** Operations on [glob_constr] *) val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option |