diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-22 20:16:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-22 20:16:05 +0000 |
| commit | 3d6a65d54f9703357e7f232de30a460404c983bd (patch) | |
| tree | 046c4240b31139b7d9a142a38b1ff0ba9a2a7b37 /toplevel | |
| parent | 23d402abfa076a5e4f9b538bc4c314884c02b0e4 (diff) | |
Stringmap -> Idmap
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 42f05a01d..6712e900f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -288,10 +288,8 @@ let push_inductive_names ccitab sp mie = let _,ccitab = List.fold_left (fun (p,ccitab) x -> - (p+1, - Stringmap.add (string_of_id x) (ConstructRef (indsp,p)) - ccitab)) - (1,Stringmap.add (string_of_id id) (IndRef indsp) ccitab) + (p+1, Idmap.add x (ConstructRef (indsp,p)) ccitab)) + (1,Idmap.add id (IndRef indsp) ccitab) ind.mind_entry_consnames in (n+1,ccitab)) (0,ccitab) @@ -322,8 +320,7 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function | sp,Leaf obj -> begin match object_tag obj with | "CONSTANT" | "PARAMETER" -> - (Stringmap.add (string_of_id (basename sp)) - (ConstRef sp) ccitab,objtab,modtab) + (Idmap.add (basename sp) (ConstRef sp) ccitab,objtab,modtab) | "INDUCTIVE" -> let mie = out_inductive obj in (push_inductive_names ccitab sp mie, objtab, modtab) @@ -338,16 +335,14 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function (* ou quelque chose comme cela *) | "CLASS" | "COERCION" | "STRUCTURE" | "OBJDEF1" | "SYNTAXCONSTANT" | _ -> - (ccitab, - Stringmap.add (string_of_id (basename sp)) (sp,obj) objtab, - modtab) + (ccitab, Idmap.add (basename sp) (sp,obj) objtab, modtab) end | _,(ClosedSection _ | OpenedSection _ | FrozenState _ | Module _) -> tabs and segment_contents seg = let ccitab, objtab, modtab = List.fold_left process_object - (Stringmap.empty, Stringmap.empty, Stringmap.empty) + (Idmap.empty, Idmap.empty, Stringmap.empty) seg in Nametab.Closed (ccitab, objtab, modtab) @@ -355,7 +350,7 @@ and segment_contents seg = let close_section _ s = let oldenv = Global.env() in let sec_sp,decls,fs = close_section false s in - let newdir = dirpath sec_sp in + let newdir = dirpath (* Trick for HELM *) sec_sp in let olddir = wd_of_sp sec_sp in let (ops,ids,_) = if Options.immediate_discharge then ([],[],([],[],[])) |