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 /contrib/romega | |
| 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 'contrib/romega')
| -rw-r--r-- | contrib/romega/const_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index c358e593d..c64038323 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -64,7 +64,7 @@ let recognize_number t = let constant dir s = try Declare.global_absolute_reference - (Names.make_path (List.map Names.id_of_string dir) + (Names.make_path (Names.make_dirpath (List.map Names.id_of_string dir)) (Names.id_of_string s) Names.CCI) with e -> print_endline (String.concat "." dir); print_endline s; raise e |