diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index af2834e498..aa48516aff 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -20,12 +20,12 @@ val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t +val cases_pattern_loc : cases_pattern -> Loc.t option 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 +val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -42,7 +42,8 @@ val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t -val loc_of_glob_constr : glob_constr -> Loc.t +(* Obsolete *) +val loc_of_glob_constr : glob_constr -> Loc.t option val glob_visible_short_qualid : glob_constr -> Id.t list (* Renaming free variables using a renaming map; fails with |