From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Mar 2018 20:29:16 +0100
Subject: [api] Deprecate a couple of aliases that we missed.

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a0d69ce796..e3832a48e1 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
-- 
cgit v1.2.3