diff options
| author | Hugo Herbelin | 2020-04-08 17:23:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-11 10:41:09 +0200 |
| commit | 33aaa5d64771c3644de4771338c371ce6b865647 (patch) | |
| tree | 9784941fee1c59152986afc988118d82a921c8de /interp/constrextern.ml | |
| parent | 9aefd708109658a8a17412e1fd7cc95bff454050 (diff) | |
If a custom entry has global, a bound variable is valid in this entry.
This is due to "global" being a syntactic notation, thus including ident.
Parsing was automatically supporting this. This commit adds support for printing.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0396e556cf..a37bac3275 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> let loc = pat.CAst.loc in match DAst.get pat with - | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Name id) when entry_has_global custom || entry_has_ident custom -> + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) | pat -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -935,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r = match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) -> + CAst.make ?loc (extern_var ?loc id) | c -> |