diff options
| author | barras | 2002-02-14 15:54:01 +0000 |
|---|---|---|
| committer | barras | 2002-02-14 15:54:01 +0000 |
| commit | 909d7c9edd05868d1fba2dae65e6ff775a41dcbe (patch) | |
| tree | 7a9c1574e278535339336290c1839db09090b668 /pretyping/detyping.ml | |
| parent | 67f72c93f5f364591224a86c52727867e02a8f71 (diff) | |
- Reforme de la gestion des args recursifs (via arbres reguliers)
- coqtop -byte -opt bouclait!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6d12257b3c..8e5e35930b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -15,6 +15,7 @@ open Names open Term open Declarations open Inductive +open Inductiveops open Environ open Sign open Declare @@ -34,17 +35,9 @@ let encode_inductive ref = errorlabstrm "indsp_of_id" (pr_global_env (Global.env()) ref ++ str" is not an inductive type") in - let (mib,mip) = Global.lookup_inductive indsp in - let constr_lengths = Array.map List.length mip.mind_listrec in + let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) -let constr_nargs indsp = - let (mib,mip) = Global.lookup_inductive indsp in - let nparams = mip.mind_nparams in - Array.map - (fun t -> List.length (fst (decompose_prod_assum t)) - nparams) - mip.mind_nf_lc - (* Parameterization of the translation from constr to ast *) (* Tables for Cases printing under a "if" form, a "let" form, *) @@ -110,10 +103,10 @@ module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet) let force_let ci = let indsp = ci.ci_ind in - let lc = constr_nargs indsp in PrintingLet.active (indsp,lc) + let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc) let force_if ci = let indsp = ci.ci_ind in - let lc = constr_nargs indsp in PrintingIf.active (indsp,lc) + let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc) (* Options for printing or not wildcard and synthetisable types *) @@ -235,7 +228,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 = constr_nargs indsp in + let consnargsl = mis_constr_nargs indsp in let pred = if synth_type & computable p k & considl <> [||] then None |