diff options
| author | herbelin | 2000-07-01 17:44:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-01 17:44:37 +0000 |
| commit | 04457e0084f3887c7d5c0ed072e26ac53ce20382 (patch) | |
| tree | faf17b791cbad3938c39dd9eece30ac67714f13a /tactics | |
| parent | ffaf841c89505bfc0d5a898344a5f1c8c5bf724c (diff) | |
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 4 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 02e35d4f2d..22bc94b691 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -462,7 +462,7 @@ let descend_then sigma env head dirn = (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> - let aritysign,_ = get_arity env sigma indf in + let aritysign,_ = get_arity indf in let p = lam_it (lift (mis_nrealargs mispec) resty) aritysign in let build_branch i = let result = if i = dirn then dirnval else dfltval in @@ -500,7 +500,7 @@ let construct_discriminator sigma env dirn c sort = errorlabstrm "Equality.construct_discriminator" [< 'sTR "Cannot discriminate on inductive constructors with dependent types" >] in - let arsign,arsort = get_arity env sigma indf in + let arsign,arsort = get_arity indf in let (true_0,false_0,sort_0) = match necessary_elimination arsort (destSort sort) with | Type_Type -> build_UnitT (), build_EmptyT (), (Type dummy_univ) @@ -524,7 +524,7 @@ let rec build_discriminator sigma env dirn c sort = function let cty = type_of env sigma c in let IndType (indf,_) = try find_rectype env sigma cty with Not_found -> assert false in - let _,arsort = get_arity env sigma indf in + let _,arsort = get_arity indf in let nparams = mis_nparams (fst (dest_ind_family indf)) in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in let newc = Rel(cnum_nlams-(argnum-nparams)) in diff --git a/tactics/inv.ml b/tactics/inv.ml index d7de3df9be..385cd574cd 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -93,7 +93,7 @@ let make_inv_predicate env sigma ind id status concl = match status with | NoDep -> (* We push the arity and leave concl unchanged *) - let hyps_arity,_ = get_arity env sigma indf in + let hyps_arity,_ = get_arity indf in let env' = push_rels hyps_arity env in (hyps_arity,concl) | Dep dflt_concl -> @@ -108,7 +108,7 @@ let make_inv_predicate env sigma ind id status concl = | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> let sort = get_sort_of env sigma concl in - let p = make_arity env sigma true indf sort in + let p = make_arity env true indf sort in abstract_list_all env sigma p concl (realargs@[VAR id]) in let hyps,_ = decompose_lam pred in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 281c1eb189..60a4cd3647 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -149,7 +149,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let p = next_ident_away (id_of_string "P") allvars in let pty,goal = if dep_option then - let pty = make_arity env sigma true indf sort in + let pty = make_arity env true indf sort in let goal = mkProd Anonymous (mkAppliedInd ind) (applist(VAR p,realargs@[Rel 1])) in |