diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb66658a37..701c07dc8d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -107,7 +107,7 @@ let _show_inactive_notations () = let deactivate_notation nr = match nr with | SynDefRule kn -> - (* shouldn't we check wether it is well defined? *) + (* shouldn't we check whether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with @@ -757,11 +757,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType _ as s when !print_universes -> s - | GType _ -> GType [] + (* In case we print a glob_constr w/o having passed through detyping *) + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed _ when not !print_universes -> UAnonymous {rigid=true} + | UNamed _ | UAnonymous _ as u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -1312,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort Sorts.InSProp -> GSort GSProp - | PSort Sorts.InProp -> GSort GProp - | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType []) + | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0]) + | PSort Sorts.InProp -> GSort (UNamed [GProp,0]) + | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) + | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i let extern_constr_pattern env sigma pat = |