diff options
| author | Hugo Herbelin | 2019-11-14 08:26:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:15 +0100 |
| commit | 14196d8ab425f67faf3995bd29a003de3b2e87ac (patch) | |
| tree | 37379c35029ee6269a9796f42f360e329b4f9a23 /interp/constrintern.ml | |
| parent | 556e9dde62b6822db20bd5c7e6e6a67bc717c408 (diff) | |
Propagate implicit arguments in all notations for partial applications.
This was done for abbreviations but not string notations. This adopts
the policy proposed in #11091 to make parsing and printing consistent.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1cfd50e26e..e14629df9b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2070,9 +2070,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref - | CNotation (_,ntn,([],[],[],[])) -> + | CNotation (_,ntn,ntnargs) -> assert (Option.is_empty isproj); - let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in + let c = intern_notation intern env ntnvars loc ntn ntnargs in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in |