From f83572bc45b9ab6b72688eb22d125896541ccf16 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Sep 2001 16:55:41 +0000
Subject: 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
---
 tactics/tacticals.ml  | 6 +++---
 tactics/tacticals.mli | 2 +-
 tactics/tactics.ml    | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6e3d331218..168cd94e1c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -313,9 +313,9 @@ let elimination_sort_of_goal gl =
   match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
     | IsSort s ->
 	(match s with
-	   | Prop Null -> ElimOnProp
-	   | Prop Pos -> ElimOnSet
-	   | Type _ -> ElimOnType)
+	   | Prop Null -> InProp
+	   | Prop Pos -> InSet
+	   | Type _ -> InType)
     | _        -> anomaly "goal should be a type"
 
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 54b66539b8..2451a89794 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -119,7 +119,7 @@ type branch_assumptions = {
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
   indargs   : identifier list} (* the inductive arguments *)
 
-val elimination_sort_of_goal : goal sigma -> Declarations.elimination_sorts
+val elimination_sort_of_goal : goal sigma -> sorts_family
 (*i val suff              : goal sigma -> constr -> string i*)
 
 val general_elim_then_using :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f168cb5cb0..18cb8ee509 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1067,7 +1067,7 @@ let default_elim (c,lbindc)  gl =
            pr_id id; 'sPC;
 	   'sTR "The elimination of the inductive definition :";
            pr_id base; 'sPC; 'sTR "on sort "; 
-           'sPC; print_sort (Declarations.sort_of_elimination s) ;
+           'sPC; print_sort (new_sort_in_family s) ;
 	   'sTR " is probably not allowed" >]
   in  general_elim (c,lbindc) (elimc,[]) gl
 
-- 
cgit v1.2.3