Commit 5905eaba authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added access to package version from Coq.

parent 2da689fd
......@@ -31,5 +31,5 @@ AC_SUBST(COQRFLAG, ['-R . Flocq'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into a Flocq module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile src/Makefile])
AC_CONFIG_FILES([Makefile src/Makefile src/Flocq_version.v])
AC_OUTPUT
Require Import BinNat.
Require Import Ascii String.
Definition Flocq_version := Eval vm_compute in
let fix parse s major minor :=
match s with
| String "."%char t => parse t (major * 100 + minor)%N N0
| String h t => parse t major (minor + N_of_ascii h - N_of_ascii "0"%char)%N
| Empty_string => (major * 100 + minor)%N
end in
parse "@PACKAGE_VERSION@"%string N0 N0.
FILES = \
Flocq_version.v \
Core/Fcore_defs.v \
Core/Fcore_float_prop.v \
Core/Fcore_Raux.v \
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment