diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 12:49:19 +0000 |
| commit | a6d858b84132bcb27bcc771f06a854cc94eef716 (patch) | |
| tree | df016a77a6d8d2f2a43fa9c2c01adc09b3be7c1b /toplevel/discharge.ml | |
| parent | 000ece141dc22e35365ea81558e8b6b1e65bd54c (diff) | |
Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 01b868aa2..f6d96e292 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -310,9 +310,8 @@ let catch_not_found f x = 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 olddir = wd_of_sp sec_sp in + let olddir,decls,fs = close_section false s in + let newdir = fst (split_dirpath olddir) in let (ops,ids,_) = List.fold_left (process_item oldenv newdir olddir) ([],[],([],[],[])) decls |