diff options
| author | Matthieu Sozeau | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /interp | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
3 files changed, 6 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 36fa81157a..d51d067b28 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -595,8 +595,8 @@ let extern_optimal_prim_token scopes r r' = let extern_glob_sort = function | GProp -> GProp | GSet -> GSet - | GType (Some _) as s when !print_universes -> s - | GType _ -> GType None + | GType _ as s when !print_universes -> s + | GType _ -> GType [] let extern_universes = function | Some _ as l when !print_universes -> l diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8f76bbb61b..7db2203c08 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1360,7 +1360,9 @@ let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef (ref,us) as x -> let (c,imp,subscopes,l),isproj,_ = - intern_applied_reference intern env (Environ.named_context globalenv) lvar us [] ref in + intern_applied_reference intern env (Environ.named_context globalenv) + lvar us [] ref + in apply_impargs (None, isproj) c env imp subscopes l (constr_loc x) | CFix (loc, (locid,iddef), dl) -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5cad2b54d6..9461cebb0f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -731,7 +731,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> match_in u alp metas sigma c1 c2 - | GSort (_,GType _), NSort (GType None) when not u -> sigma + | GSort (_,GType _), NSort (GType _) when not u -> sigma | GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma |