diff options
| author | herbelin | 2001-09-19 16:55:41 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-19 16:55:41 +0000 |
| commit | f83572bc45b9ab6b72688eb22d125896541ccf16 (patch) | |
| tree | 37e08a39ea53751d9fdd7dff4449f4125e3f7bfd /parsing | |
| parent | 3607bb83605ff596445e0f18016d1fbb3d66d584 (diff) | |
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 6 | ||||
| -rw-r--r-- | parsing/astterm.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 3017a6aee8..9b537f70e8 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -706,9 +706,9 @@ let interp_sort = function | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >]) let interp_elimination_sort = function - | Node(loc,"PROP", []) -> Declarations.ElimOnProp - | Node(loc,"SET", []) -> Declarations.ElimOnSet - | Node(loc,"TYPE", _) -> Declarations.ElimOnType + | Node(loc,"PROP", []) -> InProp + | Node(loc,"SET", []) -> InSet + | Node(loc,"TYPE", _) -> InType | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >]) let judgment_of_rawconstr sigma env c = diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 4503f09a6a..1941439c75 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -26,7 +26,7 @@ val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr val interp_type : 'a evar_map -> env -> Coqast.t -> types val interp_sort : Coqast.t -> sorts -val interp_elimination_sort : Coqast.t -> Declarations.elimination_sorts +val interp_elimination_sort : Coqast.t -> sorts_family val interp_openconstr : 'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr |