diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-15 16:36:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-15 16:36:15 +0000 |
| commit | 3636d52354226848ef89fbe4539cfa4e5daaa170 (patch) | |
| tree | 5aaffe68b3e99966e74a06002f96cd719d8a5465 /pretyping/inductiveops.ml | |
| parent | bda9e8da3320c3d54be356878c8d8cd9b3caec11 (diff) | |
Suppression argument pattern_source du case_info (code jamais utilisé)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 041187d84..69f921b79 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -131,21 +131,16 @@ let allowed_sorts env (kn,i as ind) = mip.mind_kelim (* Annotation for cases *) -let make_case_info env ind style pats_source = +let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let print_info = - { ind_nargs = mip.mind_nrealargs; - style = style; - source = pats_source } in + let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in { ci_ind = ind; ci_npar = mib.mind_nparams; ci_cstr_nargs = mip.mind_consnrealdecls; ci_pp_info = print_info } let make_default_case_info env style ind = - let (mib,mip) = Inductive.lookup_mind_specif env ind in make_case_info env ind style - (Array.map (fun _ -> RegularPat) mip.mind_consnames) (*s Useful functions *) |