diff options
| author | herbelin | 2000-07-01 17:53:48 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-01 17:53:48 +0000 |
| commit | a51f67a717a93cf61bfed79e70da9f35555dcab7 (patch) | |
| tree | 34789ed013f1edd5669f2db84bff8cddb63567a8 /library | |
| parent | c6edcac49bc32e12106e576430c3251d78276f8e (diff) | |
Précalcul de la forme canonique des constructeurs et arités pour traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 4 | ||||
| -rw-r--r-- | library/indrec.ml | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 5b52f19760..bae96bc141 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -67,8 +67,8 @@ let inductives_table = ref Spmap.empty let declare_inductive_implicits sp = let mib = Global.lookup_mind sp in let imps_one_inductive mip = - (auto_implicits (body_of_type mip.mind_arity), - Array.map (fun c -> auto_implicits (body_of_type c)) mip.mind_lc) + (auto_implicits (mind_user_arity mip), + Array.map (fun c -> auto_implicits c) (mind_user_lc mip)) in let imps = Array.map imps_one_inductive mib.mind_packets in inductives_table := Spmap.add sp imps !inductives_table diff --git a/library/indrec.ml b/library/indrec.ml index da5aeec345..d24ce2aa6a 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -52,7 +52,7 @@ let mis_make_case_com depopt env sigma mispec kind = if k = mis_nconstr mispec then let nbprod = k+1 in let ind = make_ind_family (mispec,rel_list nbprod nparams) in - let lnamesar,_ = get_arity env' sigma ind in + let lnamesar,_ = get_arity ind in let ci = make_default_case_info mispec in it_lambda_name env' (lambda_create env' @@ -69,7 +69,7 @@ let mis_make_case_com depopt env sigma mispec kind = (add_branch (k+1)) in let indf = make_ind_family (mispec,rel_list 0 nparams) in - let typP = make_arity env' sigma dep indf kind in + let typP = make_arity env' dep indf kind in it_lambda_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar (* check if the type depends recursively on one of the inductive scheme *) @@ -210,7 +210,7 @@ let mis_make_indrec env sigma listdepkind mispec = (* arity in the context P1..P_nrec f1..f_nbconstruct *) let params = rel_list (nrec+nbconstruct) nparams in let indf = make_ind_family (mispeci,params) in - let lnames,_ = get_arity env sigma indf in + let lnames,_ = get_arity indf in let nar = mis_nrealargs mispeci in let decf = nar+nrec+nbconstruct+nrec in @@ -281,7 +281,7 @@ let mis_make_indrec env sigma listdepkind mispec = let rec put_arity i = function | (mispeci,dep,kinds)::rest -> let indf = make_ind_family (mispeci,rel_list i nparams) in - let typP = make_arity env sigma dep indf kinds in + let typP = make_arity env dep indf kinds in mkLambda_string "P" typP (put_arity (i+1) rest) | [] -> make_branch 0 listdepkind |