diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 16:55:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 16:55:41 +0000 |
| commit | f83572bc45b9ab6b72688eb22d125896541ccf16 (patch) | |
| tree | 37e08a39ea53751d9fdd7dff4449f4125e3f7bfd /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 6 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6e3d33121..168cd94e1 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 54b66539b..2451a8979 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 f168cb5cb..18cb8ee50 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 |