diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-18 01:47:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:11:01 +0200 |
| commit | c4e3c884316a1156d6707fc7011b6e2f2e7428f0 (patch) | |
| tree | 775be811eedfaca306bcdbdb5eddee0ebce42c1b | |
| parent | 2e49d4cd3f4607af2893531d15cd7eb66a8cb9b0 (diff) | |
Adapting code to renaming Array.fold_map -> Array.fold_left_map.
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a5ba9bb00..565a7e642 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -180,10 +180,10 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = 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_map (List.fold_left_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 = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in - let e',idl = Array.fold_map (to_id g) e idl in + let e',idl = Array.fold_left_map (to_id g) e idl in GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort x |