diff options
| author | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
| commit | 4fb4f1adf18648b4fb561986379e033b00423148 (patch) | |
| tree | 876f561f9310b9e15f3ac20ca71f9dd28f90b157 /library | |
| parent | 349944eb8e3abd51dc2b94051a887253a2ae9198 (diff) | |
| parent | de988641848ecb26f749fbc3f50ce9194db46a4c (diff) | |
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Diffstat (limited to 'library')
| -rw-r--r-- | library/globnames.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index 9d7ab2db8d..a6e75fdb6a 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -30,7 +30,7 @@ let eq_gr gr1 gr2 = | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | _ -> false + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" |