diff options
| author | Jasper Hugunin | 2019-02-16 16:47:58 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2019-02-16 17:22:50 -0800 |
| commit | 6d54c0fbbe8c905991dcb99112cce69792c9b142 (patch) | |
| tree | 92e88d00bf71bee729e4c55a26ff8a2897ff547a /vernac | |
| parent | 5ea4369bd4604b61ccc669f136827299920fb635 (diff) | |
Deprecated duplicated explicitation_eq
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |