Coq

~jgross-h/coq/+git/coq:v8.3

Last commit made on 2017-12-09
Get this branch:
git clone -b v8.3 https://git.launchpad.net/~jgross-h/coq/+git/coq

Branch merges

Branch information

Name:
v8.3
Repository:
lp:~jgross-h/coq/+git/coq

Recent commits

04a6362... by Hugo Herbelin <email address hidden>

Adding support for OCaml 4.06.0 (option -unsafe-string needed).

And other minor changes.

Cherry-pick from v8.4 (7f2240f).

81266e0... by Hugo Herbelin <email address hidden>

Updating configure with ocaml >= 4.03.0.

Warning 31 introduced in 4.00.0 makes compilation fail from 4.03.0.

It is apparently not fatal for the purpose of Coq, so we deactivate
it.

220dec9... by Hugo Herbelin <email address hidden>

Not recommending 4.02.0.

0e0077e... by Hugo Herbelin <email address hidden>

Fixing a little ennoying approximation in configure when detecting camlp5.

Cherry-pick from v8.4 (f7a96f72).

7fc1d59... by Hugo Herbelin <email address hidden>

Using explicit lablgtk2 directory in coqmktop rather than +lablgtk2
which does not work the way lablgtk2 is installed by opam.

6f7bec8... by Hugo Herbelin <email address hidden>

Ensuring that sed does not use a specific locale for characters >= 128,
so that it does not fail on files containing latin1 characters,
e.g. g_omega.ml4.

(Actually backport of 2b8fa6a51bb by Pierre B.)

d8a7832... by Hugo Herbelin <email address hidden>

v8.3: Fix for #4467 (missing shadowing of variables in cases pattern).

Backported from v8.4.

c024126... by Hugo Herbelin <email address hidden>

v8.3: Quick fix so that we can give option -lablgtkdir and the
escaping of quotes is always done for coq_config.ml (not very moral
though, that a string containing a "-I dir" string is hard-wired in
coq_config.ml which is supposed to be at a different level of
abstraction than the level of ocaml executable syntax).

cc6fe21... by Hugo Herbelin <email address hidden>

v8.3: supporting compilation of coqide with lablgtk 2.16 and 2.18.

Collapsing new Gtk modifiers to MOD5 for compatibility with lablgtk 2.14.

Not sure that this is the optimal thing to do, but, at least, this
does not seem to be changing the use of CoqIDE wrt to it was when
using lablgtk 2.14.

4bed028... by Hugo Herbelin <email address hidden>

v8.3: Fixing critical bug in typing match with let-ins in the arity.