Merge PR #9883: Add support for Sorts in numeral notations

Ack-by: SkySkimmer
Ack-by: proux01
Reviewed-by: vbgl

1 files changed, 7 insertions, 0 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 70d3e4175e..c157cf43fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -503,6 +503,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
       sigma,mkApp (c, Array.of_list cl)
   | Glob_term.GInt i -> sigma, mkInt i
+  | Glob_term.GSort gs ->
+      let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
+      sigma,mkSort c
   | _ ->
       raise NotAValidPrimToken
 
@@ -516,6 +519,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
   | Int i -> DAst.make ?loc (Glob_term.GInt i)
+  | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0]))
+  | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0]))
+  | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0]))
+  | Sort (Sorts.Type _) -> DAst.make ?loc (Glob_term.GSort (Glob_term.UAnonymous {rigid=true}))
   | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
 
 let no_such_prim_token uninterpreted_token_kind ?loc ty =