diff options
| author | Maxime Dénès | 2018-04-12 17:59:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-12 17:59:35 +0200 |
| commit | 32b142d297c3fb259d0977efdb267fdc7c99b1d7 (patch) | |
| tree | 46dc062383d3442806e345a23cb61fa837dd8ba4 /interp/notation_ops.ml | |
| parent | 485eb7958811ff627d9c50ec7a6ed36ed9416b97 (diff) | |
| parent | 0ade32f84b28d2190360ec79520788142755b5b7 (diff) | |
Merge PR #6972: [api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index aa9a6ed0d7..a76f820941 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -210,7 +210,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in |