From 8096b8167d02566658929217f4627142d98dc835 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 2 Jun 2000 12:36:41 +0000 Subject: Mise en place d'un choix constr/typed_type en remplacement de certains Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@488 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index c923cfe17..964cf0298 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -366,12 +366,11 @@ let find_positions env sigma t1 t2 = and t2_0 = applist t2_0 in if is_conv env sigma t1_0 t2_0 then [] - else - (match whd_castapp ((unsafe_machine env sigma t1_0).uj_kind) with - | DOP0(Sort(Prop Pos)) -> - [(List.rev posn,t1_0,t2_0)] (* Set *) - | DOP0(Sort(Type(_))) -> - [(List.rev posn,t1_0,t2_0)] (* Type *) + else + let ty1_0 = get_type_of env sigma t1_0 in + (match get_sort_of env sigma ty1_0 with + | Prop Pos -> [(List.rev posn,t1_0,t2_0)] (* Set *) + | Type _ -> [(List.rev posn,t1_0,t2_0)] (* Type *) | _ -> []) in (try @@ -448,9 +447,8 @@ let discriminable env sigma t1 t2 = *) let descend_then sigma env head dirn = - let headj = unsafe_machine env sigma head in let IndType (indf,_) as indt = - try find_inductive env sigma headj.uj_type + try find_inductive env sigma (get_type_of env sigma head) with Not_found -> assert false in let mispec,params = dest_ind_family indf in let construct = -- cgit v1.2.3