diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-14 22:13:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-14 22:13:07 +0000 |
| commit | 42679bb4f94de0a25d6fe5a959e00cfe7a1454d9 (patch) | |
| tree | 02bca1d940eb146b99298a5ed9182122f73160e0 /library | |
| parent | 32db56471909ae183832989670a81bf59b8a8e5c (diff) | |
Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/library/declare.ml b/library/declare.ml index 305dd815b..4d76ef8aa 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -172,36 +172,19 @@ let declare_constant id cd = let inductive_names sp mie = let names, _ = List.fold_left - (fun (names, n) (id,_,cnames,_) -> + (fun (names, n) ind -> let indsp = (sp,n) in let names, _ = List.fold_left (fun (names, p) id -> let sp = Names.make_path (dirpath sp) id CCI in ((sp, ConstructRef (indsp,p)) :: names, p+1)) - (names, 1) cnames in - let sp = Names.make_path (dirpath sp) id CCI in + (names, 1) ind.mind_entry_consnames in + let sp = Names.make_path (dirpath sp) ind.mind_entry_typename CCI in ((sp, IndRef indsp) :: names, n+1)) ([], 0) mie.mind_entry_inds in names -let push_inductive_names sp mie = - let _ = - List.fold_left - (fun n (id,_,cnames,_) -> - let indsp = (sp,n) in - let _ = - List.fold_left - (fun p id -> - let sp = Names.make_path (dirpath sp) id CCI in - Nametab.push sp (ConstructRef (indsp,p)); (p+1)) - 1 cnames in - let sp = Names.make_path (dirpath sp) id CCI in - Nametab.push sp (IndRef indsp); - n+1) - 0 mie.mind_entry_inds - in () - let check_exists_inductive (sp,_) = if Nametab.exists_cci sp then errorlabstrm "cache_inductive" @@ -230,7 +213,7 @@ let (in_inductive, out_inductive) = let declare_mind mie = let id = match mie.mind_entry_inds with - | (id,_,_,_)::_ -> id + | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in let sp = add_leaf id CCI (in_inductive mie) in |