diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 19:43:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 19:43:43 +0100 |
| commit | a4a59ec5cf426bb1ee36dc1ac49cb20bd17d5f43 (patch) | |
| tree | 466c6643c909f0df08dbc7ed8443e7283a2123e1 | |
| parent | 69f219cdcddc10823d52ffa1ea9503254e48bce4 (diff) | |
| parent | 6d54c0fbbe8c905991dcb99112cce69792c9b142 (diff) | |
Merge PR #9589: Deprecate duplicated explicitation_eq
Reviewed-by: ejgallego
Reviewed-by: herbelin
Ack-by: jashug
| -rw-r--r-- | interp/impargs.ml | 9 | ||||
| -rw-r--r-- | interp/impargs.mli | 1 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
3 files changed, 4 insertions, 8 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e8f2f4f3d..6fd52d98dd 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -120,12 +120,7 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq ex1 ex2 = match ex1, ex2 with -| ExplByPos (i1, id1), ExplByPos (i2, id2) -> - Int.equal i1 i2 && Option.equal Id.equal id1 id2 -| ExplByName id1, ExplByName id2 -> - Id.equal id1 id2 -| _ -> false +let explicitation_eq = Constrexpr_ops.explicitation_eq type implicit_explanation = | DepRigid of argument_position @@ -380,7 +375,7 @@ let flatten_explicitations l autoimps = | (Name id,_)::imps -> let value, l' = try - let eq = explicitation_eq in + let eq = Constrexpr_ops.explicitation_eq in let flags = List.assoc_f eq (ExplByName id) l in Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l with Not_found -> assoc_by_pos k l diff --git a/interp/impargs.mli b/interp/impargs.mli index 4afc2af5e9..43c26b024f 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -138,4 +138,5 @@ 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]. *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 5e74114a86..5eb19eef54 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -35,7 +35,7 @@ let check_imps ~impsty ~impsbody = try List.for_all (fun (key, (va:bool*bool*bool)) -> (* Pervasives.(=) is OK for this type *) - Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va) + Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va) impsbody with Not_found -> false in |