diff options
author | 2001-09-19 16:55:41 +0000 | |
---|---|---|
committer | 2001-09-19 16:55:41 +0000 | |
commit | f83572bc45b9ab6b72688eb22d125896541ccf16 (patch) | |
tree | 37e08a39ea53751d9fdd7dff4449f4125e3f7bfd /library/declare.ml | |
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 'library/declare.ml')
-rw-r--r-- | library/declare.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/declare.ml b/library/declare.ml index 9b6466f47..d2e451dd9 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -554,12 +554,12 @@ let instantiate_inductive_section_params t ind = (* Eliminations. *) let eliminations = - [ (ElimOnProp,"_ind") ; (ElimOnSet,"_rec") ; (ElimOnType,"_rect") ] + [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ] let elimination_suffix = function - | ElimOnProp -> "_ind" - | ElimOnSet -> "_rec" - | ElimOnType -> "_rect" + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" let make_elimination_ident id s = add_suffix id (elimination_suffix s) @@ -583,7 +583,7 @@ let declare_one_elimination mispec = List.iter (fun (sort,suff) -> if List.mem sort kelim then - declare (mindstr^suff) (make_elim (sort_of_elimination sort))) + declare (mindstr^suff) (make_elim (new_sort_in_family sort))) eliminations let declare_eliminations sp = |