aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/subtac_utils.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-23 15:08:21 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-23 15:08:21 +0000
commit7ddef6f71e017af324113ae43c0fe2a5abc09764 (patch)
treec0b01889d0e274dcd7ff07e5e84019b90c4e3699 /plugins/subtac/subtac_utils.ml
parentaa9a5fddd49c9bec13d178f274f24dabcc033850 (diff)
Fix commit 14489: missing Coq. in dirpath
Kudos to Tom Prince for noticing this... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14491 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac_utils.ml')
-rw-r--r--plugins/subtac/subtac_utils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index cf90074c9..ae28c9847 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -22,7 +22,7 @@ let init_constant dir s () = gen_constant contrib_name dir s
let init_reference dir s () = gen_reference contrib_name dir s
let safe_init_constant md name () =
- check_required_library md;
+ check_required_library ("Coq"::md);
init_constant md name ()
let ex_pi1 = init_constant utils_module "ex_pi1"