diff options
| author | Hugo Herbelin | 2020-04-12 21:31:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | 0f434208acc9e16382839f343b45d24aeaba0afd (patch) | |
| tree | 6eb23c0d67e439a47e965c6114d448d9508a07c9 /interp | |
| parent | 6e884b01deaf2b9a7d012590c9e3f103d4091c4d (diff) | |
Removing a useless explicit use of subscopes in interpreting arguments of a notation.
Diffstat (limited to 'interp')
| -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 d4090117b0..c7c298cd5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1822,8 +1822,8 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> ensure_kind test_kind ?loc g; - let (argscs1,argscs2) = find_remaining_scopes pl args g in - let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in + let (_,argscs2) = find_remaining_scopes pl args g in + let pl = List.map (in_not test_kind_inner loc scopes fullsubst []) pl in let pl = add_local_defs_and_check_length loc genv g pl args in let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in let pat = |