aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 7b62ef166..6a21e451d 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -47,8 +47,13 @@ let init () =
let i = ref 0
let version () =
- Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nCompiled on %s\n"
+ Printf.sprintf "The Coq Proof Assistant, version %s (%s)\nConfigured on %s\nThis is the %s version (%s is the best one) for architecture %s on system %s
+Gtk version is %s"
Coq_config.version Coq_config.date Coq_config.compile_date
+ (if Mltop.get () = Mltop.Native then "native" else "byte")
+ (if Coq_config.best="opt" then "native" else "byte")
+ Coq_config.arch Sys.os_type
+ (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
let is_in_coq_lib dir =
prerr_endline ("Is it a coq theory ? : "^dir);