diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 11:36:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:57 +0100 |
| commit | c1cab3ba606f7034f2785f06c0d3892bca3976cf (patch) | |
| tree | 19918420f7e4b64be31953dae8f51c981e638f4a /interp/constrextern.ml | |
| parent | 745eb8d6d9f99b69d11c16e8fb5e133e8e27d0a8 (diff) | |
Removing cumbersome location in multiple patterns.
This is to have a better symmetry between CCases and GCases.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bc8debd02..6704ed4b7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -967,7 +967,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], + Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function |