diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533..ac2118ba7 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -25,7 +25,7 @@ val cases_pattern_loc : cases_pattern -> Loc.t 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 |