diff options
| author | herbelin | 2000-05-05 13:24:02 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-05 13:24:02 +0000 |
| commit | 40be348f4502976adc0a7612e9dcf489cfd19330 (patch) | |
| tree | eabe0259378f58ea3e5cd67753f490d17fd092dc | |
| parent | 29b2b65a4ac3154860189b6123b561bed3d16c15 (diff) | |
ajout interp_sort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@425 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 : |