diff options
| author | Pierre-Marie Pédrot | 2017-07-24 18:40:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-24 18:41:27 +0200 |
| commit | fed8f69b682c03ff901966890efd2d9d3ea91004 (patch) | |
| tree | cee4ffd2fb34d8b45d6e5d0ad0ec10bec57cb127 /src | |
| parent | c25e86e6b4e8bb694d3c8e50f04a92cc33ad807d (diff) | |
Fix library hardwired prefix.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2env.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2env.ml b/src/tac2env.ml index 5ccdd018ee..08c7b321be 100644 --- a/src/tac2env.ml +++ b/src/tac2env.ml @@ -235,7 +235,7 @@ let interp_ml_object t = MLType.obj t (** Absolute paths *) let coq_prefix = - MPfile (DirPath.make (List.map Id.of_string ["Init"; "ltac2"; "Coq"])) + MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"])) (** Generic arguments *) |