diff options
| author | Hugo Herbelin | 2018-11-14 10:10:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-01 18:00:39 +0200 |
| commit | 460bf801123d13e8c82503a2fc491892f8eed6d5 (patch) | |
| tree | 1abb0e786b727e5947ab2a5e5708d02a712a8593 /interp/notation_ops.ml | |
| parent | 45352e43db4c67eab23517f13e94ba1b5cc11808 (diff) | |
Allowing Set to be part of universe expressions.
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
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 |