diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:58:31 +0200 |
| commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
| tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /plugins/micromega/coq_micromega.ml | |
| parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
| parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) | |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a980d963..6376d023 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1434,7 +1434,7 @@ let micromega_gen (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" ^ "Unfortunately this instance of Coq isn't aware of the presence of any \"csdp\" executable. \n\n" - ^ "You may need to specify the location during Coq's pre-compilation configuration step")) gl + ^ "This executable should be in PATH")) gl let lift_ratproof prover l = match prover l with |