diff options
| author | letouzey | 2002-12-13 13:00:23 +0000 |
|---|---|---|
| committer | letouzey | 2002-12-13 13:00:23 +0000 |
| commit | 5d6b0f10b4a4a314ee48bfa3b743a3dbec521e37 (patch) | |
| tree | d21605dd2d4e1fcbb078b802bc3ef6bf5c62737c | |
| parent | 4f13345b8cf7e0af122a06ecf1a61dab8bb39175 (diff) | |
correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand meme Global.env()
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3429 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/detyping.ml | 16 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
3 files changed, 16 insertions, 7 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2758dcff48..4c6d24833b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -236,7 +236,7 @@ let rec detype tenv avoid env t = let indsp = annot.ci_ind in let considl = annot.ci_pp_info.cnames in let k = annot.ci_pp_info.ind_nargs in - let consnargsl = mis_constr_nargs indsp in + let consnargsl = mis_constr_nargs_env tenv indsp in let pred = if synth_type & computable p k & considl <> [||] then None @@ -248,12 +248,14 @@ let rec detype tenv avoid env t = array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in let eqnl = Array.to_list eqnv in let tag = - if PrintingLet.active (indsp,consnargsl) then - LetStyle - else if PrintingIf.active (indsp,consnargsl) then - IfStyle - else - annot.ci_pp_info.style + try + if PrintingLet.active (indsp,consnargsl) then + LetStyle + else if PrintingIf.active (indsp,consnargsl) then + IfStyle + else + annot.ci_pp_info.style + with Not_found -> annot.ci_pp_info.style in if tag = RegularStyle then RCases (dummy_loc,pred,[tomatch],eqnl) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e3a536420b..60700d295b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -78,6 +78,11 @@ let mis_constr_nargs indsp = let recargs = dest_subterms mip.mind_recargs in Array.map List.length recargs +let mis_constr_nargs_env env (kn,i) = + let mib = Environ.lookup_mind kn env in + let mip = mib.mind_packets.(i) in + let recargs = dest_subterms mip.mind_recargs in + Array.map List.length recargs (* Annotation for cases *) let make_case_info env ind style pats_source = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 4c5c58a9f2..23d0a32ca5 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -42,6 +42,8 @@ val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr val mis_constr_nargs : inductive -> int array +val mis_constr_nargs_env : env -> inductive -> int array + type constructor_summary = { cs_cstr : constructor; cs_params : constr list; |