diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-22 13:09:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-22 13:09:40 +0000 |
| commit | 5923919582bbfa207d5141d5059bd3916e501843 (patch) | |
| tree | 9f439b72d43f7cc6d7552e7dbe7456fb0295dff6 /toplevel/mltop.ml4 | |
| parent | 2fa42e57ecc5e8170e36fb63919f4b0a9ad19430 (diff) | |
- Fixed minor bug #1994 in the tactic chapter of the manual [doc]
- Improved warning when found several path to the same file in path
[mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
[Datatypes.v, tactics]
PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/mltop.ml4')
| -rw-r--r-- | toplevel/mltop.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 275f9a5f7..694e60dbc 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -106,7 +106,7 @@ let dir_ml_load s = * if this code section starts to use a module not used elsewhere * in this file, the Makefile dependency logic needs to be updated. *) - let _,gname = where_in_path true !coq_mlpath_copy s in + let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in try Dynlink.loadfile gname; with | Dynlink.Error a -> |