diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-02 12:36:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-02 12:36:41 +0000 |
| commit | 8096b8167d02566658929217f4627142d98dc835 (patch) | |
| tree | bf5966fc3128644f3c0d9cdf6e5ab0d01ad8672a /tactics | |
| parent | 374b73b66f0356dd3204818458ec916584e750dc (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 14 |
1 files changed, 6 insertions, 8 deletions
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 = |