aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/impargs.mli2
-rw-r--r--interp/notation_ops.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1eeb8e41a..103a4f9e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -130,7 +130,7 @@ val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
-val projection_implicits : env -> projection -> implicit_status list ->
+val projection_implicits : env -> Projection.t -> implicit_status list ->
implicit_status list
val select_impargs_size : int -> implicits_list list -> implicit_status list
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index aa9a6ed0d..a76f82094 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