diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /pretyping/glob_ops.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9b2da0b084..e14766f370 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -148,7 +148,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Array.equal f c1 c2 && Array.equal f t1 t2 | GSort s1, GSort s2 -> glob_sort_eq s1 s2 | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Option.equal (==) gn1 gn2 (* Only thing sensible *) && Namegen.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 |