diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-04 16:58:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-04 16:58:33 +0000 |
| commit | 1c6747af716224b092b0f197772bc6bcc186293b (patch) | |
| tree | e8fe986a8e46435f893d891e7e1ee05e6e83b550 /pretyping | |
| parent | 783bdffba901a29027878f41e10b6bcfe406100f (diff) | |
Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 8 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fd6a0457d..2fbfa70f7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -190,7 +190,7 @@ type 'a pattern_matching_problem = (* Utils *) let to_mutind env sigma t = - try IsInd (t,try_mutind_of env sigma t) + try IsInd (t,find_inductive env sigma t) with Induc -> NotInd t let type_of_tomatch_type = function @@ -831,18 +831,18 @@ let coerce_row typing_fun isevars env row tomatch = (let tyi = inductive_of_rawconstructor c in try let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in - IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type) + IsInd (j.uj_type,find_inductive env !isevars j.uj_type) with NotCoercible -> (* 2 cas : pas le bon inductive ou pas un inductif du tout *) try - let ind_data = try_mutind_of env !isevars j.uj_type in + let ind_data = find_inductive env !isevars j.uj_type in error_bad_constructor_loc cloc CCI (constructor_of_rawconstructor c) ind_data.mind with Induc -> error_case_not_inductive_loc (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type) | None -> - try IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type) + try IsInd (j.uj_type,find_inductive env !isevars j.uj_type) with Induc -> NotInd (j.uj_type) in (j.uj_val,t) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8462a72f6..340129813 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -397,7 +397,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | ROldCase (loc,isrec,po,c,lf) -> let cj = pretype empty_tycon env isevars lvar lmeta c in let {mind=mind;params=params;realargs=realargs} = - try try_mutind_of env !isevars cj.uj_type + try find_inductive env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in let pj = match po with diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 67c131524..0e61614b3 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -53,7 +53,7 @@ let rec type_of env cstr= let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ | IsMutCase (_,p,c,lf) -> let ind_data = - try try_mutind_of env sigma (type_of env c) + try find_inductive env sigma (type_of env c) with Induc -> anomaly "type_of: Bad inductive" in let (aritysign,_) = get_arity env sigma ind_data in let (psign,_) = splay_prod env sigma (type_of env p) in |