From cd7e8284c7defdad636ffa7ef87f3e584a7592fb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 1 Apr 2019 16:25:31 -0400
Subject: Add support for Sorts in numeral notations

---
 interp/notation.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'interp/notation.ml')

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 =
-- 
cgit v1.2.3