diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.mli | 4 |
4 files changed, 3 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e5bf52571c..bb66658a37 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -850,10 +850,10 @@ let rec extern inctx scopes vars r = | Some c :: q -> match locs with | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | (_, false) :: locs' -> + | { Recordops.pk_true_proj = false } :: locs' -> (* we don't want to print locals *) ip q locs' args acc - | (_, true) :: locs' -> + | { Recordops.pk_true_proj = true } :: locs' -> match args with | [] -> raise No_match (* we give up since the constructor is not complete *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c0801067ce..f06493b374 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer = let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch.") - | (_, regular) :: proj_kinds -> + | { Recordops.pk_true_proj = regular } :: proj_kinds -> (* "regular" is false when the field is defined by a let-in in the record declaration (its value is fixed from other fields). *) diff --git a/interp/impargs.ml b/interp/impargs.ml index d83a0ce918..90fb5a2036 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq = Constrexpr_ops.explicitation_eq - type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position diff --git a/interp/impargs.mli b/interp/impargs.mli index 0070423530..ccdd448460 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -143,7 +143,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list -> val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list - -val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool - [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"] -(** Equality on [explicitation]. *) |