diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c967f4e884..91a2ef9c1e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -101,5 +101,4 @@ val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t val empty_lvar : Ltac_pretype.ltac_var_map |