diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 17:57:28 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 17:57:28 +0200 |
| commit | d7dc4d4082d76e480b6d9932dcfad64249565e80 (patch) | |
| tree | 47c24efb25606259c3e0d9c2ac4da2160880a47e /pretyping/glob_ops.mli | |
| parent | 510879170dae6edb989c76a96ded0ed00f192173 (diff) | |
| parent | f713e6c195d1de177b43cab7c2902f5160f6af9f (diff) | |
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 75db04f77..6bb421e73 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -83,3 +83,6 @@ val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list + +val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name +val empty_lvar : Glob_term.ltac_var_map |