diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 7 |
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 = |