diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 2e8908cfb..730332514 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -24,7 +24,7 @@ val glob_sort_eq : glob_sort -> glob_sort -> bool val cases_pattern_loc : cases_pattern -> Loc.t -val cases_predicate_names : tomatch_tuples -> name list +val cases_predicate_names : tomatch_tuples -> Name.t list (** Apply one argument to a glob_constr *) val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr @@ -46,6 +46,6 @@ val loc_of_glob_constr : glob_constr -> Loc.t Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern +val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern -val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr +val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr |