diff options
| author | Gaëtan Gilbert | 2019-06-06 13:27:40 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-06 13:27:40 +0200 |
| commit | 90c1084ba489415f8df588c43e088491bc6be450 (patch) | |
| tree | 0489f116505f9956d7fd076937038009dbc0485e /interp/notation_ops.ml | |
| parent | 4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff) | |
| parent | 1ac8d4751317d50b01a53980b09f36c5dc30c8e3 (diff) | |
Merge PR #8988: Towards unifying parsing/printing for universe instances and Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7f084fffdd..08619d912e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 - | GSort (GType _), NSort (GType _) when not u -> sigma + + (* Next pair of lines useful only if not coming from detyping *) + | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match + | GSort _, NSort (UAnonymous _) when not u -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match |