diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-12 17:59:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-12 17:59:35 +0200 |
| commit | 32b142d297c3fb259d0977efdb267fdc7c99b1d7 (patch) | |
| tree | 46dc062383d3442806e345a23cb61fa837dd8ba4 /interp | |
| parent | 485eb7958811ff627d9c50ec7a6ed36ed9416b97 (diff) | |
| parent | 0ade32f84b28d2190360ec79520788142755b5b7 (diff) | |
Merge PR #6972: [api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
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 |