diff options
| -rw-r--r-- | parsing/astterm.ml | 5 | ||||
| -rw-r--r-- | parsing/astterm.mli | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index bdb0f17138..5f90c309c2 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -524,6 +524,11 @@ let interp_constr_gen is_ass sigma env com = let interp_constr sigma env c = interp_constr_gen false sigma env c let interp_type sigma env c = interp_constr_gen true sigma env c +let interp_sort = function + | Node(loc,"PROP", []) -> Prop Null + | Node(loc,"SET", []) -> Prop Pos + | Node(loc,"TYPE", []) -> Type Univ.dummy_univ + | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >]) let judgment_of_com sigma env com = let c = interp_rawconstr sigma env com in diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 46c8f5b665..6c50a5ebd5 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -20,6 +20,8 @@ val interp_type : 'a evar_map -> env -> Coqast.t -> constr val typed_type_of_com : 'a evar_map -> env -> Coqast.t -> typed_type val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment +val interp_sort : Coqast.t -> sorts + (*Interprets a constr according to two lists of instantiations (variables and metas)*) val interp_constr1 : |